如何定义仅允许使用十六进制字符的
subtype
或 String
?这是我的尝试,但我在子类型定义上失败了:
subtype Hex_Character is Character
with Static_Predicate => Hex_Character in
'A' .. 'F' | 'a' .. 'f' | '0' .. '9';
subtype Hex_String is String ...;
您可以添加动态谓词:
main.adb
procedure Main with SPARK_Mode is
subtype Hex_Character is Character
with Static_Predicate => Hex_Character in
'A' .. 'F' | 'a' .. 'f' | '0' .. '9';
subtype Hex_String is String
with Dynamic_Predicate =>
(for all Char of Hex_String => Char in Hex_Character);
S1 : Hex_String := "ABCDEF1234567890"; -- Line 11
S2 : Hex_String := "Foo"; -- Line 12
begin
null;
end Main;
输出(GNAT证明)
$ gnatprove -Pdefault.gpr -u main.adb --level=1 --report=all
Phase 1 of 3: generation of data representation information ...
Phase 2 of 3: generation of Global contracts ...
Phase 3 of 3: flow analysis and proof ...
main.adb:11:23: info: predicate check proved
main.adb:12:23: medium: predicate check might fail, cannot prove Char in Hex_Character
12 | S2 : Hex_String := "Foo";
| ^~~~~
in inlined predicate at main.adb:9
Summary logged in ./obj/gnatprove/gnatprove.out