Ada 中仅包含十六进制字符的字符串子类型

问题描述 投票:0回答:1

如何定义仅允许使用十六进制字符的

subtype
String
?这是我的尝试,但我在子类型定义上失败了:

subtype Hex_Character is Character
  with Static_Predicate => Hex_Character in 
     'A' .. 'F' | 'a' .. 'f' | '0' .. '9';
subtype Hex_String is String ...;
ada
1个回答
0
投票

您可以添加动态谓词:

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
最新问题
© www.soinside.com 2019 - 2024. All rights reserved.