examples/tests-provers/strings.mlw

   1
   2 module TestString
   3
   4   use string.String
   5   use int.Int
   6
   7   goal Empty: "" = ""
   8
   9   goal Empty2: empty = ""
  10
  11   goal Test0: not ("a" = "b")
  12
  13   constant a: string
  14
  15   goal Test1:
  16     (if 2 + 2 = 4 then "a" = a else "b" = a) -> "a" = a
  17     (* this should be proved even with alt-ergo due to the sharing of
  18        literals *)
  19
  20   goal Test2:
  21     let a = if 2 + 2 = 4 then "a" else "" in
  22     let b = if 2 + 2 = 4 then "b" else "" in
  23     not (a = b)
  24
  25   goal Test3:
  26     let a = if 2 + 2 = 4 then "a" else "" in
  27     let b = if 2 + 2 = 4 then "a" else "" in
  28     a = b
  29
  30   goal Test4:
  31     let s = "abcdef" in substring s 2 3 = "cde"
  32
  33   goal TestConcat1:
  34     let s1 = "abc" in
  35     let s2 = "defg" in
  36     concat s1 s2 = "abcdefg"
  37
  38   goal TestConcat5:
  39     concat "" "" = ""
  40
  41   goal TestLength1: length "a" = 1
  42   goal TestLength2: length "ab" = 2
  43   goal TestLength3: length "abc" = 3
  44   goal TestLength4: length (concat "ab" "12") = 4
  45   (* TODO \xC3\xA9 is the encoding of 'é' *)
  46   (* TODO goal TestLength5: length "\xC3\xA9" = 2 *)
  47
  48   goal TestLt1: lt "" "a"
  49   goal TestLt2: lt "a" "b"
  50   goal TestLt3: lt "ab" "b"
  51   goal TestLt4: lt "abcde" "b"
  52   goal TestLt5: lt "a" "1"
  53   goal TestLt6: lt "A" "a"
  54
  55   goal TestLT: not (lt "" "")
  56   goal TestLE: not (le "A" "")
  57
  58   goal TestAt1:
  59     s_at "abc" 3 = empty
  60
  61   goal TestSubstring1:
  62     substring "abcdef" 1 3 = "bcd"
  63
  64   goal TestSubstring2:
  65     substring "abcdef" 1 10 = "bcdef"
  66
  67   goal containsTest1: contains "" ""
  68
  69   goal substring_contains: forall s1 s2.
  70     contains s1 s2 -> exists i. substring s1 i (length s2) = s2
  71
  72   goal TestIndefof1:
  73     indexof "" "" 0 = 0
  74
  75   goal TestIndefof2:
  76     indexof "a" "" 0 = 0
  77
  78   goal TestIndefof3:
  79     indexof "" "a" 0 = -1
  80
  81   goal TestIndefof4:
  82     indexof "a" "" 1 = 1
  83
  84   goal TestIndefof5:
  85     indexof "a" "" 2 = -1
  86
  87   goal TestIndefof6:
  88     indexof "ab" "" 2 = 2
  89
  90   goal TestIndefof7:
  91     indexof "abcdef" "c" 0 = 2
  92
  93   goal TestIndefof8:
  94     indexof "abcdef" "c" 2 = 2
  95
  96   goal TestIndefof9:
  97     indexof "abcdef" "c" 3 = -1
  98
  99   goal TestIndefof10:
 100     indexof "abcdef" "cdef" 0 = 2
 101
 102   goal TestIndexof11: forall s1.
 103     indexof s1 "" 0 = 0
 104
 105   goal TestReplace1: forall s2 s3.
 106    s2 <> "" -> replace "" s2 s3 = ""
 107
 108   goal TestReplace2: forall s1 s3. (* check standard to see if this makes sense *)
 109    replace s1 "" s3 = concat s3 s1
 110
 111   goal TestReplace3:
 112    replace "abcde" "bc" "1234" = "a1234de"
 113
 114   goal TestReplace4:
 115    replace "abcdefg" "fg" "" = "abcde"
 116
 117   goal TestReplace5:
 118    replace "abcdefabcdef" "bc" "123" = "a123defabcdef"
 119
 120   goal to_int_lt_0: forall s i.
 121     0 <= i < length s && lt (s_at s i) "0"
 122         -> to_int s = -1
 123
 124   goal to_int_gt_9: forall s i.
 125     0 <= i < length s && lt "9" (s_at s i)
 126         -> to_int s = -1
 127
 128   goal TestIsDigit:
 129     is_digit "0" && is_digit "1" && is_digit "2" && is_digit "3" &&
 130     is_digit "4" && is_digit "5" && is_digit "6" && is_digit "7" &&
 131     is_digit "8" && is_digit "9"
 132
 133   goal TestIsDigit2:
 134     not (is_digit "00") && not (is_digit "q") && not (is_digit "-1") &&
 135     not (is_digit "10") && not (is_digit "!") && not (is_digit "\xAA")
 136
 137   goal TestTo_int1: to_int "1" = 1
 138   goal TestTo_int2: to_int "11" = 11
 139   goal TestTo_int3: to_int "123" = 123
 140   goal TestTo_int4: to_int "" = -1
 141   goal TestTo_int5: to_int "a" = -1
 142   goal TestTo_int6: to_int "-1" = -1
 143   goal TestTo_int7: to_int "-2" = -1
 144   goal TestTo_int8: to_int "-11" = -1
 145   goal TestTo_int9: to_int "1a1" = -1
 146
 147   goal TestFrom_int: from_int 1 = "1"
 148
 149   goal TestProvedInAltergo1: forall s1 s2.
 150     length s1 = length (concat s1 s2) -> s2 = ""
 151
 152   (* proved with alt-ergo but not with CVC4 *)
 153   goal TestProvedInAltergo2: forall s1 s2.
 154     prefixof s1 s2 -> exists i. substring s2 0 i = s1
 155   (*** TODO: axioms about to_int -- the following are not proved *)
 156
 157 end
 158
 159 module TestInput
 160
 161   use string.String
 162
 163   goal T0: length "this is a test" = 14
 164   goal T1: length "\x17" = 1
 165   goal T2: length "\o027" = 1
 166   goal T3: length "\023" = 1
 167   goal T4: length "\t" = 1
 168   goal T5: length "\\" = 1
 169   goal T6: length "\"" = 1
 170   goal T7: length "\n" = 1
 171   (* goal T8: length "\p" = 1 *)
 172   (*   goal T9: length "a *)
 173   (* b" = 2 *)
 174   goal T10: length "'" = 1
 175   goal T11: length "/" = 1
 176   goal T12: length "`" = 1
 177   (* à is the same as \195\160 *)
 178   (* goal T13: length "à" = 1 *)
 179   (* goal T14: length "Ϯ" = 1 *)
 180   (* á is the same as \195\161, \o303\o241, \xC3\xA1 *)
 181   (* goal T15: length "á" = 1 *)
 182   goal T16: length "\o303\o241" = 2
 183   goal T17: length "\xC3\xA1" = 2
 184   (* goal T18: length "\o477" = 2 *)
 185   goal T19: length "\xFFA" = 2
 186   goal T20: length "\000" = 1
 187   goal T21: length "\161" = 1
 188   goal T22: length "\r" = 1
 189   goal T23: length "'" = 1
 190   (* goal T24: length "\256" = 2 *)
 191   goal T25: length "this \
 192                     is a \
 193                     test" = 14
 194   goal T26: length "\065" = 1
 195   goal T27: length "\x41" = 1
 196   goal T28: length "\o101" = 1
 197   goal T29: "A" = "\065" = "\x41" = "\o101"
 198
 199 end
 200
 201 module TestRegExpr
 202   use string.String as S
 203   use string.RegExpr
 204
 205   (* in_re and to_re *)
 206   goal TestIn1:
 207     in_re "a" (to_re "a")
 208
 209   goal TestIn2:
 210     in_re "abc" (to_re "abc")
 211
 212   goal TestIn3:
 213     not (in_re "abc" (to_re "abd"))
 214
 215   lemma TestToReInRe: forall s.
 216     in_re s (to_re s)
 217
 218   (* concat *)
 219
 220   goal TestConcat1:
 221     let r1 = to_re "a" in
 222     let r2 = to_re "b" in
 223     in_re "ab" (concat r1 r2)
 224
 225   goal TestConcat2:
 226     let r1 = to_re "a" in
 227     let r2 = to_re "b" in
 228     not (in_re "ba" (concat r1 r2))
 229
 230   goal TestConcat3:
 231     let r1 = to_re "abc" in
 232     let r2 = to_re "def" in
 233     in_re "abcdef" (concat r1 r2)
 234
 235   goal TestConcat4:
 236     let r1 = to_re "a" in
 237     in_re (S.concat "a" "a") (concat r1 r1)
 238
 239   lemma concat: forall s1 s2.
 240     let r1 = to_re s1 in
 241     let r2 = to_re s2 in
 242     in_re (S.concat s1 s2) (concat r1 r2)
 243
 244   goal concat_exists: forall s r1 r2.
 245     in_re s (concat r1 r2) -> exists s1 s2.
 246       S.concat s1 s2 = s && in_re s1 r1 && in_re s2 r2
 247
 248   (* union *)
 249
 250   goal TestUnion1:
 251     let r1 = to_re "a" in
 252     let r2 = to_re "b" in
 253     in_re "a" (union r1 r2) && in_re "b" (union r1 r2)
 254
 255   goal TestUnion2:
 256     let r1 = to_re "a" in
 257     forall re. in_re "a" (union r1 re) && in_re "a" (union re r1)
 258
 259   goal in_union1: forall s1 r1 r2.
 260     in_re s1 r1 -> in_re s1 (union r1 r2)
 261
 262   goal in_union2: forall s1 r1 r2.
 263     in_re s1 r2 -> in_re s1 (union r1 r2)
 264
 265   goal in_union: forall s1 r1 r2.
 266     in_re s1 r1 || in_re s1 r2 -> in_re s1 (union r1 r2)
 267
 268   (* inter *)
 269
 270   goal TestInter1:
 271     let r1 = to_re "a" in
 272     let r2 = to_re "b" in
 273     not (in_re "a" (inter r1 r2))
 274
 275   goal TestInter2:
 276     let r1 = to_re "a" in
 277     let r = to_re "b" in
 278     let r2 = union r1 r in
 279     in_re "a" (inter r1 r2)
 280
 281   lemma in_inter1: forall s1:string, r1:re, r2:re.
 282     in_re s1 (inter r1 r2) -> in_re s1 r1
 283
 284   lemma in_inter2: forall s1:string, r1:re, r2:re.
 285     in_re s1 (inter r1 r2) -> in_re s1 r2
 286
 287   (* star *)
 288
 289   goal TestInStar1:
 290     let a = star (to_re "a") in
 291     in_re "aaa" a &&
 292     not (in_re "aba" a)
 293
 294   goal TestInStar2:
 295     let a = to_re "a" in
 296     let b = to_re "b" in
 297     let ab = star (union a b) in
 298     in_re "a" ab &&
 299     in_re "b" ab &&
 300     in_re "babab" ab &&
 301     in_re "baaa" ab &&
 302     in_re "aaaa" ab &&
 303     in_re "bbbb" ab &&
 304     not (in_re "acaab") ab
 305
 306   goal TestDigit:
 307     let d = union (to_re "0") (union (to_re "1") (union (to_re "2")
 308            (union (to_re "3") (union (to_re "4") (union (to_re "5")
 309            (union (to_re "6") (union (to_re "7") (union (to_re "8")
 310             (to_re "9"))))))))) in
 311     let ds = star d in
 312     let is_digit x = in_re x d in
 313     let are_digits x = in_re x ds in
 314     is_digit "1" && is_digit "9" && is_digit "0" &&
 315     not (is_digit "a") && not (is_digit "12") &&
 316     are_digits "0" && are_digits "4" && are_digits "9" &&
 317     are_digits "1850" && are_digits "10" && are_digits "000" &&
 318     not (are_digits "1 ") && not (are_digits " 1") &&
 319     not (are_digits "1a") && not (are_digits "a1") &&
 320     not (are_digits "a")
 321
 322   goal star1: forall s re.
 323     in_re s re -> in_re s (star re)
 324
 325   lemma star2: forall re.
 326     in_re S.empty (star re)
 327
 328   (* plus *)
 329
 330   goal TestPlus1:
 331     let a = plus (to_re "a") in
 332     in_re "a" a && in_re "aaa" a && not (in_re "b" a) &&
 333     not (in_re "ab" a) && not (in_re "" a)
 334
 335   lemma def_plus: forall re.
 336     plus re = concat re (star re)
 337
 338   goal plus_star: forall s r.
 339     in_re s (plus r) -> in_re s (star r)
 340
 341   (* none, all, allchar *)
 342
 343   goal TestAllChar:
 344     in_re "a" allchar && in_re "1" allchar && in_re "!" allchar &&
 345     not (in_re "aa" allchar) && not (in_re "!!" allchar)
 346
 347   goal TestAll:
 348     in_re "as 3hoiqjndhfgasohn123^*&(T@GIGDSOA" all
 349
 350   lemma allchar: forall s.
 351     S.length s = 1 -> in_re s allchar
 352
 353   lemma in_re_none: forall s: string.
 354     not (in_re s none)
 355
 356   lemma all_allchar: forall s.
 357     in_re s (star allchar)
 358
 359   lemma in_re_all: forall s.
 360     in_re s all
 361
 362   lemma union_all: forall r.
 363     union all r = union r all = all
 364
 365   lemma inter_all: forall r.
 366     inter r all = inter all r = r
 367
 368   lemma star_all: star all = all
 369
 370   (* opt *)
 371
 372   goal TestOpt1:
 373     let a = to_re "a" in
 374     in_re "a" (opt a) && in_re "" (opt a) && not (in_re "ab" (opt a))
 375
 376   lemma empty_opt: forall re.
 377     in_re "" (opt re)
 378
 379   lemma in_opt: forall s.
 380     in_re s (opt (to_re s))
 381
 382   (* range *)
 383
 384   goal TestRange1:
 385     in_re "b" (range "a" "c") &&
 386     in_re "b" (range "b" "c") &&
 387     in_re "b" (range "a" "b") &&
 388     not (in_re "d" (range "a" "c"))
 389
 390   goal TestRange2:
 391     not (in_re "abc" (range "a" "b"))
 392
 393   goal range_negative: forall s.
 394     not (in_re s (range "b" "a"))
 395
 396   goal range_not_singleton: forall s.
 397     not (in_re s (range "ba" "a"))
 398
 399   (* power, loop *)
 400
 401   goal TestPower1:
 402     let a = to_re "a" in
 403     in_re "aa" (power 2 a)
 404
 405   goal TestPower2:
 406     let ab = to_re "ab" in
 407     in_re "ababab" (power 3 ab)
 408
 409   goal TestPower3: forall i.
 410     let ab = to_re "ab" in
 411     in_re "ababab" (power i ab)
 412
 413   goal TestLoop1:
 414     let a = to_re "a" in
 415     in_re "aa" (loop 2 3 a)
 416
 417
 418
 419 end