Commit 872879a7 by Jean-Christophe Filliâtre

### programs: as a side-effect of the new for loop, the syntax 'variant {t} for R'...

`programs: as a side-effect of the new for loop, the syntax 'variant {t} for R' is changed into 'variant {t} with R' (no big deal, it is rarely used)`
parent 1e3a525c
 ... ... @@ -5,7 +5,7 @@ logic rel int int } let rec even (x:int) : int variant {x} for rel = let rec even (x:int) : int variant {x} with rel = odd (x-1) and odd (x:int) : int variant {x} = even (x-1) ... ...
 ... ... @@ -29,7 +29,7 @@ let f91_nonrec (n x : ref int) = label L: while !n > 0 do invariant { !n >= 0 and iter_f !n !x = iter_f (at !n L) (at !x L) } variant { (101 - !x + 10 * !n, !n) } for lex variant { (101 - !x + 10 * !n, !n) } with lex if !x > 100 then begin x := !x - 10; n := !n - 1 ... ...
 ... ... @@ -83,49 +83,36 @@ let search () = (forall i:int. n <= i < m -> !x#i = 0) } label Init: let s = ref 0 in let i = ref 0 in while !i < m do (* could be n instead of m *) invariant { 0 <= !i <= m and !s = sum_digits (interp !x 0 !i) } variant { m - !i } s := !s + array_get x !i; i := !i + 1 for i = 0 to m - 1 do (* could be n instead of m *) invariant { !s = sum_digits (interp !x 0 i) } s := !s + array_get x i done; assert { !s = sum_digits (interp !x 0 m) }; let d = ref 0 in while !d < m do for d = 0 to m - 1 do invariant { 0 <= !d <= m and !x = at !x Init and !s = sum_digits (interp !x !d m) !x = at !x Init and !s = sum_digits (interp !x d m) } variant { m - !d } let c = ref (array_get x !d) in while !c <= 9 do invariant { !x # !d <= !c <= 10 and !x = at !x Init } variant { 10 - !c } let delta = y - !s - !c + array_get x !d in if 0 <= delta && delta <= 9 * !d then begin array_set x !d !c; assert { sum_digits (interp !x !d m) = y - delta }; for c = array_get x d + 1 to 9 do invariant { !x = at !x Init } let delta = y - !s - c + array_get x d in if 0 <= delta && delta <= 9 * d then begin array_set x d c; assert { sum_digits (interp !x d m) = y - delta }; let k = div delta 9 in assert { k <= !d }; i := 0; while !i < k do invariant { 0 <= !i <= k and A.length !x = m } variant { k - !i } array_set x !i 9; i := !i + 1 assert { k <= d }; for i = 0 to k - 1 do invariant { A.length !x = m } array_set x i 9 done; array_set x !i (mod delta 9); i := !i + 1; while !i < !d do invariant { k+1 <= !i and A.length !x = m } variant { !d - !i } array_set x !i 0; i := !i + 1 array_set x k (mod delta 9); for i = k + 1 to d - 1 do invariant { A.length !x = m } array_set x i 0 done; assume { sum_digits (interp !x 0 !d) = delta }; assume { sum_digits (interp !x 0 d) = delta }; raise Success end; c := !c + 1 end done; s := !s - array_get x !d; d := !d + 1 s := !s - array_get x d done { true(*false*) } | Success -> ... ...
 ... ... @@ -582,9 +582,9 @@ opt_raises: ; opt_variant: | /* epsilon */ { None } | VARIANT LOGIC { Some (\$2, id_lt_nat ()) } | VARIANT LOGIC FOR lqualid { Some (\$2, \$4) } | /* epsilon */ { None } | VARIANT LOGIC { Some (\$2, id_lt_nat ()) } | VARIANT LOGIC WITH lqualid { Some (\$2, \$4) } ; opt_cast: ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!