mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
420 lines
9.7 KiB
Plaintext
420 lines
9.7 KiB
Plaintext
|
|
module TestString
|
|
|
|
use string.String
|
|
use int.Int
|
|
|
|
goal Empty: "" = ""
|
|
|
|
goal Empty2: empty = ""
|
|
|
|
goal Test0: not ("a" = "b")
|
|
|
|
constant a: string
|
|
|
|
goal Test1:
|
|
(if 2 + 2 = 4 then "a" = a else "b" = a) -> "a" = a
|
|
(* this should be proved even with alt-ergo due to the sharing of
|
|
literals *)
|
|
|
|
goal Test2:
|
|
let a = if 2 + 2 = 4 then "a" else "" in
|
|
let b = if 2 + 2 = 4 then "b" else "" in
|
|
not (a = b)
|
|
|
|
goal Test3:
|
|
let a = if 2 + 2 = 4 then "a" else "" in
|
|
let b = if 2 + 2 = 4 then "a" else "" in
|
|
a = b
|
|
|
|
goal Test4:
|
|
let s = "abcdef" in substring s 2 3 = "cde"
|
|
|
|
goal TestConcat1:
|
|
let s1 = "abc" in
|
|
let s2 = "defg" in
|
|
concat s1 s2 = "abcdefg"
|
|
|
|
goal TestConcat5:
|
|
concat "" "" = ""
|
|
|
|
goal TestLength1: length "a" = 1
|
|
goal TestLength2: length "ab" = 2
|
|
goal TestLength3: length "abc" = 3
|
|
goal TestLength4: length (concat "ab" "12") = 4
|
|
(* TODO \xC3\xA9 is the encoding of 'é' *)
|
|
(* TODO goal TestLength5: length "\xC3\xA9" = 2 *)
|
|
|
|
goal TestLt1: lt "" "a"
|
|
goal TestLt2: lt "a" "b"
|
|
goal TestLt3: lt "ab" "b"
|
|
goal TestLt4: lt "abcde" "b"
|
|
goal TestLt5: lt "a" "1"
|
|
goal TestLt6: lt "A" "a"
|
|
|
|
goal TestLT: not (lt "" "")
|
|
goal TestLE: not (le "A" "")
|
|
|
|
goal TestAt1:
|
|
s_at "abc" 3 = empty
|
|
|
|
goal TestSubstring1:
|
|
substring "abcdef" 1 3 = "bcd"
|
|
|
|
goal TestSubstring2:
|
|
substring "abcdef" 1 10 = "bcdef"
|
|
|
|
goal containsTest1: contains "" ""
|
|
|
|
goal substring_contains: forall s1 s2.
|
|
contains s1 s2 -> exists i. substring s1 i (length s2) = s2
|
|
|
|
goal TestIndefof1:
|
|
indexof "" "" 0 = 0
|
|
|
|
goal TestIndefof2:
|
|
indexof "a" "" 0 = 0
|
|
|
|
goal TestIndefof3:
|
|
indexof "" "a" 0 = -1
|
|
|
|
goal TestIndefof4:
|
|
indexof "a" "" 1 = 1
|
|
|
|
goal TestIndefof5:
|
|
indexof "a" "" 2 = -1
|
|
|
|
goal TestIndefof6:
|
|
indexof "ab" "" 2 = 2
|
|
|
|
goal TestIndefof7:
|
|
indexof "abcdef" "c" 0 = 2
|
|
|
|
goal TestIndefof8:
|
|
indexof "abcdef" "c" 2 = 2
|
|
|
|
goal TestIndefof9:
|
|
indexof "abcdef" "c" 3 = -1
|
|
|
|
goal TestIndefof10:
|
|
indexof "abcdef" "cdef" 0 = 2
|
|
|
|
goal TestIndexof11: forall s1.
|
|
indexof s1 "" 0 = 0
|
|
|
|
goal TestReplace1: forall s2 s3.
|
|
s2 <> "" -> replace "" s2 s3 = ""
|
|
|
|
goal TestReplace2: forall s1 s3. (* check standard to see if this makes sense *)
|
|
replace s1 "" s3 = concat s3 s1
|
|
|
|
goal TestReplace3:
|
|
replace "abcde" "bc" "1234" = "a1234de"
|
|
|
|
goal TestReplace4:
|
|
replace "abcdefg" "fg" "" = "abcde"
|
|
|
|
goal TestReplace5:
|
|
replace "abcdefabcdef" "bc" "123" = "a123defabcdef"
|
|
|
|
goal to_int_lt_0: forall s i.
|
|
0 <= i < length s && lt (s_at s i) "0"
|
|
-> to_int s = -1
|
|
|
|
goal to_int_gt_9: forall s i.
|
|
0 <= i < length s && lt "9" (s_at s i)
|
|
-> to_int s = -1
|
|
|
|
goal TestIsDigit:
|
|
is_digit "0" && is_digit "1" && is_digit "2" && is_digit "3" &&
|
|
is_digit "4" && is_digit "5" && is_digit "6" && is_digit "7" &&
|
|
is_digit "8" && is_digit "9"
|
|
|
|
goal TestIsDigit2:
|
|
not (is_digit "00") && not (is_digit "q") && not (is_digit "-1") &&
|
|
not (is_digit "10") && not (is_digit "!") && not (is_digit "\xAA")
|
|
|
|
goal TestTo_int1: to_int "1" = 1
|
|
goal TestTo_int2: to_int "11" = 11
|
|
goal TestTo_int3: to_int "123" = 123
|
|
goal TestTo_int4: to_int "" = -1
|
|
goal TestTo_int5: to_int "a" = -1
|
|
goal TestTo_int6: to_int "-1" = -1
|
|
goal TestTo_int7: to_int "-2" = -1
|
|
goal TestTo_int8: to_int "-11" = -1
|
|
goal TestTo_int9: to_int "1a1" = -1
|
|
|
|
goal TestFrom_int: from_int 1 = "1"
|
|
|
|
goal TestProvedInAltergo1: forall s1 s2.
|
|
length s1 = length (concat s1 s2) -> s2 = ""
|
|
|
|
(* proved with alt-ergo but not with CVC4 *)
|
|
goal TestProvedInAltergo2: forall s1 s2.
|
|
prefixof s1 s2 -> exists i. substring s2 0 i = s1
|
|
(*** TODO: axioms about to_int -- the following are not proved *)
|
|
|
|
end
|
|
|
|
module TestInput
|
|
|
|
use string.String
|
|
|
|
goal T0: length "this is a test" = 14
|
|
goal T1: length "\x17" = 1
|
|
goal T2: length "\o027" = 1
|
|
goal T3: length "\023" = 1
|
|
goal T4: length "\t" = 1
|
|
goal T5: length "\\" = 1
|
|
goal T6: length "\"" = 1
|
|
goal T7: length "\n" = 1
|
|
(* goal T8: length "\p" = 1 *)
|
|
(* goal T9: length "a *)
|
|
(* b" = 2 *)
|
|
goal T10: length "'" = 1
|
|
goal T11: length "/" = 1
|
|
goal T12: length "`" = 1
|
|
(* à is the same as \195\160 *)
|
|
(* goal T13: length "à" = 1 *)
|
|
(* goal T14: length "Ϯ" = 1 *)
|
|
(* á is the same as \195\161, \o303\o241, \xC3\xA1 *)
|
|
(* goal T15: length "á" = 1 *)
|
|
goal T16: length "\o303\o241" = 2
|
|
goal T17: length "\xC3\xA1" = 2
|
|
(* goal T18: length "\o477" = 2 *)
|
|
goal T19: length "\xFFA" = 2
|
|
goal T20: length "\000" = 1
|
|
goal T21: length "\161" = 1
|
|
goal T22: length "\r" = 1
|
|
goal T23: length "'" = 1
|
|
(* goal T24: length "\256" = 2 *)
|
|
goal T25: length "this \
|
|
is a \
|
|
test" = 14
|
|
goal T26: length "\065" = 1
|
|
goal T27: length "\x41" = 1
|
|
goal T28: length "\o101" = 1
|
|
goal T29: "A" = "\065" = "\x41" = "\o101"
|
|
|
|
end
|
|
|
|
module TestRegExpr
|
|
use string.String as S
|
|
use string.RegExpr
|
|
|
|
(* in_re and to_re *)
|
|
goal TestIn1:
|
|
in_re "a" (to_re "a")
|
|
|
|
goal TestIn2:
|
|
in_re "abc" (to_re "abc")
|
|
|
|
goal TestIn3:
|
|
not (in_re "abc" (to_re "abd"))
|
|
|
|
lemma TestToReInRe: forall s.
|
|
in_re s (to_re s)
|
|
|
|
(* concat *)
|
|
|
|
goal TestConcat1:
|
|
let r1 = to_re "a" in
|
|
let r2 = to_re "b" in
|
|
in_re "ab" (concat r1 r2)
|
|
|
|
goal TestConcat2:
|
|
let r1 = to_re "a" in
|
|
let r2 = to_re "b" in
|
|
not (in_re "ba" (concat r1 r2))
|
|
|
|
goal TestConcat3:
|
|
let r1 = to_re "abc" in
|
|
let r2 = to_re "def" in
|
|
in_re "abcdef" (concat r1 r2)
|
|
|
|
goal TestConcat4:
|
|
let r1 = to_re "a" in
|
|
in_re (S.concat "a" "a") (concat r1 r1)
|
|
|
|
lemma concat: forall s1 s2.
|
|
let r1 = to_re s1 in
|
|
let r2 = to_re s2 in
|
|
in_re (S.concat s1 s2) (concat r1 r2)
|
|
|
|
goal concat_exists: forall s r1 r2.
|
|
in_re s (concat r1 r2) -> exists s1 s2.
|
|
S.concat s1 s2 = s && in_re s1 r1 && in_re s2 r2
|
|
|
|
(* union *)
|
|
|
|
goal TestUnion1:
|
|
let r1 = to_re "a" in
|
|
let r2 = to_re "b" in
|
|
in_re "a" (union r1 r2) && in_re "b" (union r1 r2)
|
|
|
|
goal TestUnion2:
|
|
let r1 = to_re "a" in
|
|
forall re. in_re "a" (union r1 re) && in_re "a" (union re r1)
|
|
|
|
goal in_union1: forall s1 r1 r2.
|
|
in_re s1 r1 -> in_re s1 (union r1 r2)
|
|
|
|
goal in_union2: forall s1 r1 r2.
|
|
in_re s1 r2 -> in_re s1 (union r1 r2)
|
|
|
|
goal in_union: forall s1 r1 r2.
|
|
in_re s1 r1 || in_re s1 r2 -> in_re s1 (union r1 r2)
|
|
|
|
(* inter *)
|
|
|
|
goal TestInter1:
|
|
let r1 = to_re "a" in
|
|
let r2 = to_re "b" in
|
|
not (in_re "a" (inter r1 r2))
|
|
|
|
goal TestInter2:
|
|
let r1 = to_re "a" in
|
|
let r = to_re "b" in
|
|
let r2 = union r1 r in
|
|
in_re "a" (inter r1 r2)
|
|
|
|
lemma in_inter1: forall s1:string, r1:re, r2:re.
|
|
in_re s1 (inter r1 r2) -> in_re s1 r1
|
|
|
|
lemma in_inter2: forall s1:string, r1:re, r2:re.
|
|
in_re s1 (inter r1 r2) -> in_re s1 r2
|
|
|
|
(* star *)
|
|
|
|
goal TestInStar1:
|
|
let a = star (to_re "a") in
|
|
in_re "aaa" a &&
|
|
not (in_re "aba" a)
|
|
|
|
goal TestInStar2:
|
|
let a = to_re "a" in
|
|
let b = to_re "b" in
|
|
let ab = star (union a b) in
|
|
in_re "a" ab &&
|
|
in_re "b" ab &&
|
|
in_re "babab" ab &&
|
|
in_re "baaa" ab &&
|
|
in_re "aaaa" ab &&
|
|
in_re "bbbb" ab &&
|
|
not (in_re "acaab") ab
|
|
|
|
goal TestDigit:
|
|
let d = union (to_re "0") (union (to_re "1") (union (to_re "2")
|
|
(union (to_re "3") (union (to_re "4") (union (to_re "5")
|
|
(union (to_re "6") (union (to_re "7") (union (to_re "8")
|
|
(to_re "9"))))))))) in
|
|
let ds = star d in
|
|
let is_digit x = in_re x d in
|
|
let are_digits x = in_re x ds in
|
|
is_digit "1" && is_digit "9" && is_digit "0" &&
|
|
not (is_digit "a") && not (is_digit "12") &&
|
|
are_digits "0" && are_digits "4" && are_digits "9" &&
|
|
are_digits "1850" && are_digits "10" && are_digits "000" &&
|
|
not (are_digits "1 ") && not (are_digits " 1") &&
|
|
not (are_digits "1a") && not (are_digits "a1") &&
|
|
not (are_digits "a")
|
|
|
|
goal star1: forall s re.
|
|
in_re s re -> in_re s (star re)
|
|
|
|
lemma star2: forall re.
|
|
in_re S.empty (star re)
|
|
|
|
(* plus *)
|
|
|
|
goal TestPlus1:
|
|
let a = plus (to_re "a") in
|
|
in_re "a" a && in_re "aaa" a && not (in_re "b" a) &&
|
|
not (in_re "ab" a) && not (in_re "" a)
|
|
|
|
lemma def_plus: forall re.
|
|
plus re = concat re (star re)
|
|
|
|
goal plus_star: forall s r.
|
|
in_re s (plus r) -> in_re s (star r)
|
|
|
|
(* none, all, allchar *)
|
|
|
|
goal TestAllChar:
|
|
in_re "a" allchar && in_re "1" allchar && in_re "!" allchar &&
|
|
not (in_re "aa" allchar) && not (in_re "!!" allchar)
|
|
|
|
goal TestAll:
|
|
in_re "as 3hoiqjndhfgasohn123^*&(T@GIGDSOA" all
|
|
|
|
lemma allchar: forall s.
|
|
S.length s = 1 -> in_re s allchar
|
|
|
|
lemma in_re_none: forall s: string.
|
|
not (in_re s none)
|
|
|
|
lemma all_allchar: forall s.
|
|
in_re s (star allchar)
|
|
|
|
lemma in_re_all: forall s.
|
|
in_re s all
|
|
|
|
lemma union_all: forall r.
|
|
union all r = union r all = all
|
|
|
|
lemma inter_all: forall r.
|
|
inter r all = inter all r = r
|
|
|
|
lemma star_all: star all = all
|
|
|
|
(* opt *)
|
|
|
|
goal TestOpt1:
|
|
let a = to_re "a" in
|
|
in_re "a" (opt a) && in_re "" (opt a) && not (in_re "ab" (opt a))
|
|
|
|
lemma empty_opt: forall re.
|
|
in_re "" (opt re)
|
|
|
|
lemma in_opt: forall s.
|
|
in_re s (opt (to_re s))
|
|
|
|
(* range *)
|
|
|
|
goal TestRange1:
|
|
in_re "b" (range "a" "c") &&
|
|
in_re "b" (range "b" "c") &&
|
|
in_re "b" (range "a" "b") &&
|
|
not (in_re "d" (range "a" "c"))
|
|
|
|
goal TestRange2:
|
|
not (in_re "abc" (range "a" "b"))
|
|
|
|
goal range_negative: forall s.
|
|
not (in_re s (range "b" "a"))
|
|
|
|
goal range_not_singleton: forall s.
|
|
not (in_re s (range "ba" "a"))
|
|
|
|
(* power, loop *)
|
|
|
|
goal TestPower1:
|
|
let a = to_re "a" in
|
|
in_re "aa" (power 2 a)
|
|
|
|
goal TestPower2:
|
|
let ab = to_re "ab" in
|
|
in_re "ababab" (power 3 ab)
|
|
|
|
goal TestPower3: forall i.
|
|
let ab = to_re "ab" in
|
|
in_re "ababab" (power i ab)
|
|
|
|
goal TestLoop1:
|
|
let a = to_re "a" in
|
|
in_re "aa" (loop 2 3 a)
|
|
|
|
|
|
|
|
end
|