Commit 9e92f820 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Change label syntax from "foo" to [@foo].

The feature is not yet fully implemented (e.g. escape characters).
parent 6a36c00a
......@@ -376,7 +376,7 @@ predicate compatible_env (sigma:env) (sigmat:type_env) (pi:stack) (pit: type_sta
(forall id: mident. type_value (get_env id sigma) = get_reftype id sigmat) /\
(forall id: ident. type_value (get_stack id pi) = get_vartype id pit)
lemma type_inversion : forall v "induction":value.
lemma type_inversion : forall v [@induction]:value.
match (type_value v) with
| TYbool -> exists b: bool. v = Vbool b
| TYint -> exists n: int. v = Vint n
......@@ -393,7 +393,7 @@ lemma type_preservation :
sigmat:type_env, pit:type_stack.
type_stmt sigmat pit s1 ->
compatible_env sigma1 sigmat pi1 pit ->
("induction" one_step sigma1 pi1 s1 sigma2 pi2 s2) ->
([@induction] one_step sigma1 pi1 s1 sigma2 pi2 s2) ->
type_stmt sigmat pit s2 /\
compatible_env sigma2 sigmat pi2 pit
......@@ -460,25 +460,25 @@ predicate fresh_in_fmla (id:ident) (f:fmla) =
(* Needed for monotonicity and wp_reduction *)
lemma eval_msubst_term:
forall e "induction":term, sigma:env, pi:stack, x:mident, v:ident.
forall e [@induction]:term, sigma:env, pi:stack, x:mident, v:ident.
fresh_in_term v e ->
eval_term sigma pi (msubst_term e x v) =
eval_term (IdMap.set sigma x (get_stack v pi)) pi e
lemma eval_msubst:
forall f "induction":fmla, sigma:env, pi:stack, x:mident, v:ident.
forall f [@induction]:fmla, sigma:env, pi:stack, x:mident, v:ident.
fresh_in_fmla v f ->
(eval_fmla sigma pi (msubst f x v) <->
eval_fmla (IdMap.set sigma x (get_stack v pi)) pi f)
lemma eval_swap_term:
forall t "induction":term, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
forall t [@induction]:term, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
id1 <> id2 ->
(eval_term sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) t =
eval_term sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) t)
lemma eval_swap_gen:
forall f "induction":fmla, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
forall f [@induction]:fmla, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
id1 <> id2 ->
(eval_fmla sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) f <->
eval_fmla sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) f)
......@@ -490,13 +490,13 @@ lemma eval_swap:
eval_fmla sigma (Cons (id2,v2) (Cons (id1,v1) pi)) f)
lemma eval_term_change_free :
forall t "induction":term, sigma:env, pi:stack, id:ident, v:value.
forall t [@induction]:term, sigma:env, pi:stack, id:ident, v:value.
fresh_in_term id t ->
eval_term sigma (Cons (id,v) pi) t = eval_term sigma pi t
(* Need it for monotonicity*)
lemma eval_change_free :
forall f "induction":fmla, sigma:env, pi:stack, id:ident, v:value.
forall f [@induction]:fmla, sigma:env, pi:stack, id:ident, v:value.
fresh_in_fmla id f ->
(eval_fmla sigma (Cons (id,v) pi) f <-> eval_fmla sigma pi f)
......@@ -688,7 +688,7 @@ function wp (s:stmt) (q:fmla) : fmla =
eval_fmla sigma pi f -> eval_fmla sigma pi (wp body f)
lemma monotonicity:
forall s "induction":stmt, p q:fmla.
forall s [@induction]:stmt, p q:fmla.
valid_fmla (Fimplies p q)
-> valid_fmla (Fimplies (wp s p) (wp s q) )
......@@ -704,7 +704,7 @@ function wp (s:stmt) (q:fmla) : fmla =
*)
lemma distrib_conj:
forall s "induction":stmt, sigma:env, pi:stack, p q:fmla.
forall s [@induction]:stmt, sigma:env, pi:stack, p q:fmla.
(eval_fmla sigma pi (wp s p)) /\
(eval_fmla sigma pi (wp s q)) ->
eval_fmla sigma pi (wp s (Fand p q))
......@@ -717,7 +717,7 @@ function wp (s:stmt) (q:fmla) : fmla =
eval_fmla sigma' pi' (wp s' q)
lemma progress:
forall s "induction":stmt, sigma:env, pi:stack,
forall s [@induction]:stmt, sigma:env, pi:stack,
sigmat: type_env, pit: type_stack, q:fmla.
compatible_env sigma sigmat pi pit ->
type_stmt sigmat pit s ->
......
......@@ -186,7 +186,7 @@ function subst_expr (e:expr) (x:ident) (t:expr) : expr =
end
lemma eval_subst_expr:
forall s:state, e "induction":expr, x:ident, t:expr.
forall s:state, e [@induction]:expr, x:ident, t:expr.
eval_expr s (subst_expr e x t) =
eval_expr (IdMap.set s x (eval_expr s t)) e
......
......@@ -32,7 +32,7 @@ use import SumList
let rec sum (l: list or_integer_float) : (int, real) =
variant { l }
returns { si, sf -> si = add_int l /\ sf = add_real l }
"vc:sp"
[@vc:sp]
match l with
| Nil -> 0, 0.0
| Cons h t ->
......@@ -44,7 +44,7 @@ let rec sum (l: list or_integer_float) : (int, real) =
end
let main () =
"vc:sp"
[@vc:sp]
let l =
Cons (Integer 5) (Cons (Real 3.3) (Cons (Integer 8)
(Cons (Real 1.4) (Cons (Integer 9) Nil))))
......@@ -63,7 +63,7 @@ use import ref.Ref
let sum (l: list or_integer_float) : (int, real) =
returns { si, sf -> si = add_int l /\ sf = add_real l }
"vc:sp"
[@vc:sp]
let si = ref 0 in
let sf = ref 0.0 in
let ll = ref l in
......@@ -83,7 +83,7 @@ let sum (l: list or_integer_float) : (int, real) =
let main () =
"vc:sp"
[@vc:sp]
let l =
Cons (Integer 5) (Cons (Real 3.3) (Cons (Integer 8)
(Cons (Real 1.4) (Cons (Integer 9) Nil))))
......
......@@ -17,7 +17,7 @@ module BinarySearch
requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] }
ensures { 0 <= result < length a /\ a[result] = v }
raises { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v }
= "vc:sp"
= [@vc:sp]
let l = ref 0 in
let u = ref (length a - 1) in
while !l <= !u do
......@@ -56,7 +56,7 @@ module BinarySearchAnyMidPoint
requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] }
ensures { 0 <= result < length a /\ a[result] = v }
raises { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v }
= "vc:sp"
= [@vc:sp]
let l = ref 0 in
let u = ref (length a - 1) in
while !l <= !u do
......@@ -95,7 +95,7 @@ module BinarySearchInt32
ensures { 0 <= result < a.length /\ a[result] = v }
raises { Not_found ->
forall i:int. 0 <= i < a.length -> a[i] <> v }
= "vc:sp"
= [@vc:sp]
let l = ref 0 in
let u = ref (length a - 1) in
while !l <= !u do
......@@ -133,7 +133,7 @@ module BinarySearchBoolean
ensures { 0 <= result < a.length }
ensures { a[result] = 1 }
ensures { forall i. 0 <= i < result -> a[i] = 0 }
= "vc:sp"
= [@vc:sp]
let lo = ref 0 in
let hi = ref (length a - 1) in
while !lo < !hi do
......
......@@ -67,7 +67,7 @@ module BinomialHeap
end
lemma heaps_append:
forall h1 "induction" h2. heaps h1 -> heaps h2 -> heaps (h1 ++ h2)
forall h1 [@induction] h2. heaps h1 -> heaps h2 -> heaps (h1 ++ h2)
lemma heaps_reverse:
forall h. heaps h -> heaps (reverse h)
......@@ -89,7 +89,7 @@ module BinomialHeap
end
lemma occ_append:
forall l1 "induction" l2 x. occ x (l1 ++ l2) = occ x l1 + occ x l2
forall l1 [@induction] l2 x. occ x (l1 ++ l2) = occ x l1 + occ x l2
lemma occ_reverse:
forall x l. occ x l = occ x (reverse l)
......
theory Stmt "some_statement"
theory Stmt
use import real.Real
use import floating_point.Rounding
......
......@@ -2,7 +2,7 @@ module I19_simplint
use import int.Int
axiom H "W:non_conservative_extension:N" : forall x y z. x < y -> y < z -> x < z
axiom H [@W:non_conservative_extension:N] : forall x y z. x < y -> y < z -> x < z
goal g: 0 < 2
......
......@@ -78,7 +78,7 @@ theory Imp
(* Determinstic semantics *)
lemma ceval_deterministic_aux : forall c mi mf1. ceval mi c mf1 ->
forall mf2. ("inversion" ceval mi c mf2) -> mf1 = mf2
forall mf2. ([@inversion] ceval mi c mf2) -> mf1 = mf2
lemma ceval_deterministic : forall c mi mf1 mf2.
ceval mi c mf1 -> ceval mi c mf2 -> mf1 = mf2
......
......@@ -16,7 +16,7 @@ module Compiler_logic
function snd (p: ('a,'b)) : 'b = let (_,y) = p in y
meta rewrite_def function snd
predicate (-->) (x y:'a) = "rewrite" x = y
predicate (-->) (x y:'a) = [@rewrite] x = y
meta rewrite_def predicate (-->)
(* Unary predicates over machine states *)
......
......@@ -10,7 +10,7 @@ module FactRecursive
requires { x >= 0 }
variant { x }
ensures { result = fact x }
= "vc:sp"
= [@vc:sp]
if x = 0 then 1 else x * fact_rec (x-1)
let test0 () = fact_rec 0
......@@ -29,7 +29,7 @@ module FactImperative
let fact_imp (x:int) : int
requires { x >= 0 }
ensures { result = fact x }
= "vc:sp"
= [@vc:sp]
let y = ref 0 in
let r = ref 1 in
while !y < x do
......
......@@ -30,7 +30,7 @@ module FingerTrees
let lemma node_cons_app (nd:node 'a) (p q:list 'a)
ensures { node_cons nd (p++q) = node_cons nd p ++ q }
= match nd with Node2 _ _ -> "keep_on_simp" () | _ -> () end
= match nd with Node2 _ _ -> [@keep_on_simp] () | _ -> () end
function flatten (l:list (node 'a)) : list 'a = match l with
| Nil -> Nil
......
......@@ -12,7 +12,7 @@ module GcdBezout
requires { x >= 0 /\ y >= 0 }
ensures { result = gcd x y }
ensures { exists a b:int. a*x+b*y = result }
= "vc:sp"
= [@vc:sp]
let x = ref x in let y = ref y in
label Pre in
let ghost a = ref 1 in let ghost b = ref 0 in
......
(* Greatest common divisor, using the Euclidean algorithm *)
(** Greatest common divisor, using the Euclidean algorithm *)
module EuclideanAlgorithm
......@@ -10,7 +10,7 @@ module EuclideanAlgorithm
variant { v }
requires { u >= 0 /\ v >= 0 }
ensures { result = gcd u v }
= "vc:sp"
= [@vc:sp]
if v = 0 then
u
else
......@@ -27,7 +27,7 @@ module EuclideanAlgorithmIterative
let euclid (u0 v0: int) : int
requires { u0 >= 0 /\ v0 >= 0 }
ensures { result = gcd u0 v0 }
= "vc:sp"
= [@vc:sp]
let u = ref u0 in
let v = ref v0 in
while !v <> 0 do
......@@ -77,7 +77,7 @@ module BinaryGcd
variant { (v, u) with lex }
requires { u >= 0 /\ v >= 0 }
ensures { result = gcd u v }
= "vc:sp"
= [@vc:sp]
if v > u then binary_gcd v u else
if v = 0 then u else
if mod u 2 = 0 then
......@@ -121,7 +121,7 @@ module EuclideanAlgorithm63
variant { to_int v }
requires { u >= 0 /\ v >= 0 }
ensures { result = gcd u v }
= "vc:sp"
= [@vc:sp]
if v = 0 then
u
else
......
......@@ -9,13 +9,13 @@ module Exp
val ( +. ) (x y : t) : t
requires {t'isFinite x}
requires {t'isFinite y}
requires {"expl:no_overflow" t'isFinite (x .+ y)}
requires {[@expl:no_overflow] t'isFinite (x .+ y)}
ensures {result = x .+ y}
val ( *. ) (x y : t) : t
requires {t'isFinite x}
requires {t'isFinite y}
requires {"expl:no_overflow" t'isFinite (x .* y)}
requires {[@expl:no_overflow] t'isFinite (x .* y)}
ensures {result = x .* y}
let my_exp (x: t) : t
......
......@@ -87,7 +87,7 @@ module Lemmas
| Cons f tl -> mem_forest n f || mem_stack n tl
end
lemma mem_app: forall n st1 "induction" st2.
lemma mem_app: forall n st1 [@induction] st2.
mem_stack n (st1 ++ st2) -> mem_stack n st1 || mem_stack n st2
function size_stack (st: stack) : int = match st with
......
......@@ -224,7 +224,7 @@ module N
ensures {
value_sub x n (m+1) =
value_sub x n m + l2i (Map.get x m) * power radix (m-n) }
= "vc:sp" if n < m then value_sub_tail x (n+1) m else ()(*assert { 1+2=3 }*)
= [@vc:sp] if n < m then value_sub_tail x (n+1) m else ()(*assert { 1+2=3 }*)
let rec lemma value_sub_concat (x:map int limb) (n m l:int)
requires { n <= m <= l}
......
......@@ -13,17 +13,17 @@ module M
ensures { value result = x }
val add (x y: single) : single
requires { "expl:floating-point overflow"
requires { [@expl:floating-point overflow]
no_overflow NearestTiesToEven ((value x) +. (value y)) }
ensures { value result = round NearestTiesToEven ((value x) +. (value y))}
val sub (x y: single) : single
requires { "expl:floating-point overflow"
requires { [@expl:floating-point overflow]
no_overflow NearestTiesToEven ((value x) -. (value y)) }
ensures { value result = round NearestTiesToEven ((value x) -. (value y))}
val mul (x y: single) : single
requires { "expl:floating-point overflow"
requires { [@expl:floating-point overflow]
no_overflow NearestTiesToEven ((value x) *. (value y)) }
ensures { value result = round NearestTiesToEven ((value x) *. (value y))}
......@@ -47,15 +47,15 @@ module IEEEfloat
use import ieee_float.Float32
val add (x y: t) : t
requires { "expl:floating-point overflow" t'isFinite (x .+ y) }
requires { [@expl:floating-point overflow] t'isFinite (x .+ y) }
ensures { result = x .+ y }
val sub (x y: t) : t
requires { "expl:floating-point overflow" t'isFinite (x .- y)}
requires { [@expl:floating-point overflow] t'isFinite (x .- y)}
ensures { result = x .- y }
val mul (x y: t) : t
requires { "expl:floating-point overflow" t'isFinite (x .* y)}
requires { [@expl:floating-point overflow] t'isFinite (x .* y)}
ensures { result = x .* y }
let my_cosine (x:t) : t
......
......@@ -13,13 +13,13 @@ module Exp
val ( +. ) (x y : t) : t
requires {t'isFinite x}
requires {t'isFinite y}
requires {"expl:no_overflow" t'isFinite (x .+ y)}
requires {[@expl:no_overflow] t'isFinite (x .+ y)}
ensures {result = x .+ y}
val ( *. ) (x y : t) : t
requires {t'isFinite x}
requires {t'isFinite y}
requires {"expl:no_overflow" t'isFinite (x .* y)}
requires {[@expl:no_overflow] t'isFinite (x .* y)}
ensures {result = x .* y}
let my_exp (x: t) : t
......
......@@ -55,7 +55,7 @@ module PrimeNumbers
(** Bertrand's postulate, admitted as an axiom
(the label is there to suppress the warning issued by Why3) *)
axiom Bertrand_postulate "W:non_conservative_extension:N" :
axiom Bertrand_postulate [@W:non_conservative_extension:N] :
forall p: int. prime p -> not (no_prime_in p (2*p))
use import array.Array
......
......@@ -103,7 +103,7 @@ module Lemmas
| Cons f tl -> mem_forest n f || mem_stack n tl
end
lemma mem_app: forall n st1 "induction" st2.
lemma mem_app: forall n st1 [@induction] st2.
mem_stack n (st1 ++ st2) -> mem_stack n st1 || mem_stack n st2
function size_stack (st: stack) : int = match st with
......
......@@ -258,7 +258,7 @@ theory IsaPlanner_all
goal P7: forall n m: nat.
(n + m) - n = m
goal P8: forall k "induction" n m: nat.
goal P8: forall k [@induction] n m: nat.
(k + m) - (k + n) = (m - n)
goal P9: forall i j k: nat.
......@@ -302,7 +302,7 @@ theory IsaPlanner_all
goal P21: forall n m: nat.
n <= (n + m)
goal P22: forall a "induction" b "induction" c "induction": nat .
goal P22: forall a [@induction] b [@induction] c [@induction]: nat .
max (max a b) c = max a (max b c)
goal P23: forall a b: nat.
......@@ -329,7 +329,7 @@ theory IsaPlanner_all
goal P30: forall l: list 'a, x: 'a.
mem x (insert x l)
goal P31: forall a "induction" b "induction" c "induction": nat.
goal P31: forall a [@induction] b [@induction] c [@induction]: nat.
min (min a b) c = min a (min b c)
goal P32: forall a b: nat.
......@@ -414,18 +414,18 @@ theory IsaPlanner_beyond
goal P54: forall m n: nat.
(m + n) - n = m
goal P55: forall i "induction" k "induction" j "induction" : nat.
goal P55: forall i [@induction] k [@induction] j [@induction] : nat.
(i - j) - k = i - (k - j)
goal P56: forall xs ys: list 'a, n: nat.
drop n (xs ++ ys) = drop n xs ++ drop (n - (len xs)) ys
goal P57: forall n "induction" m "induction": nat,
xs "induction": list nat.
goal P57: forall n [@induction] m [@induction]: nat,
xs [@induction]: list nat.
drop n (drop m xs) = drop (n + m) xs
goal P58: forall xs "induction": list 'a,
m "induction" n "induction": nat.
goal P58: forall xs [@induction]: list 'a,
m [@induction] n [@induction]: nat.
drop n (take m xs) = take (m - n) (drop n xs)
end
......@@ -256,7 +256,7 @@ module BoundedIntegers
Sum.sum (fun i -> (a[i] : int)) lo hi
let maximum_subarray (a: array int63) (ghost lo hi: ref int): int63
requires { "no overflow" forall l h. 0 <= l <= h <= length a ->
requires { [@no overflow] forall l h. 0 <= l <= h <= length a ->
sum a l h <= max_int }
ensures { 0 <= !lo <= !hi <= length a && result = sum a !lo !hi }
ensures { forall l h. 0 <= l <= h <= length a -> result >= sum a !lo !hi }
......
......@@ -11,7 +11,8 @@ module McCarthy91
let rec f91 (n:int) : int variant { 101-n }
ensures { result = spec n }
= "vc:sp" if n <= 100 then
= [@vc:sp]
if n <= 100 then
f91 (f91 (n + 11))
else
n - 10
......@@ -22,7 +23,8 @@ module McCarthy91
use import int.Iter
let f91_nonrec (n0: int) ensures { result = spec n0 }
= "vc:sp" let e = ref 1 in
= [@vc:sp]
let e = ref 1 in
let n = ref n0 in
while !e > 0 do
invariant { !e >= 0 /\ iter spec !e !n = spec n0 }
......@@ -47,7 +49,8 @@ module McCarthy91
let f91_pseudorec (n0:int) : int
ensures { result = spec n0 }
= "vc:sp" let e = ref 1 in
= [@vc:sp]
let e = ref 1 in
let n = ref n0 in
let bloc () : unit
requires { !e >= 0 }
......@@ -85,7 +88,8 @@ module McCarthy91Mach
let rec f91 (n: int63) : int63
variant { 101 - n }
ensures { result = spec n }
= "vc:sp" if n <= 100 then
= [@vc:sp]
if n <= 100 then
f91 (f91 (n + 11))
else
n - 10
......@@ -96,7 +100,8 @@ module McCarthy91Mach
let f91_nonrec (n0: int63) : int63
ensures { result = spec n0 }
= "vc:sp" let e = ref one in
= [@vc:sp]
let e = ref one in
let n = ref n0 in
while gt !e zero do
invariant { !e >= 0 /\ iter spec !e !n = spec n0 }
......@@ -115,7 +120,8 @@ module McCarthy91Mach
let f91_pseudorec (n0: int63) : int63
ensures { result = spec n0 }
= "vc:sp" let e = ref one in
= [@vc:sp]
let e = ref one in
let n = ref n0 in
let bloc () : unit
requires { !e >= 0 }
......
......@@ -12,7 +12,7 @@ module FastExponentiation
let rec fast_exp x n variant { n }
requires { 0 <= n }
ensures { result = power x n }
= "vc:sp"
= [@vc:sp]
if n = 0 then
1
else begin
......@@ -27,7 +27,7 @@ module FastExponentiation
let fast_exp_imperative x n
requires { 0 <= n }
ensures { result = power x n }
= "vc:sp"
= [@vc:sp]
let r = ref 1 in
let p = ref x in
let e = ref n in
......
......@@ -107,7 +107,7 @@ module DWP
meta compute_max_steps 0x10000
predicate (-->) (x y: 'a) = "rewrite" x = y
predicate (-->) (x y: 'a) = [@rewrite] x = y
meta rewrite_def predicate (-->)
type post = state -> state -> bool
......
......@@ -315,7 +315,7 @@ module SchorrWaite
(* Need induction to recover path-based specification. *)
assert { forall x y m. m = memo at I /\ x <> null /\ y <> null /\
mem x graph /\ black memo.colors[x] ->
("induction" path m x y) -> black memo.colors[y] }
([@induction] path m x y) -> black memo.colors[y] }
end
end
\ No newline at end of file
end
......@@ -323,7 +323,7 @@ theory Extras
use import bv.BV64
lemma mod_mult: forall x "model" a "model" b "model".
lemma mod_mult: forall x [@model] a [@model] b [@model].
ule zeros x ->
ult zeros a ->
ult zeros b ->
......
......@@ -91,8 +91,8 @@ theory GappaEq2
goal G2 : forall q:double. q = result ->
value q - value q1 * value q2 <= 0x1.p-52
goal G3 : forall q:double. ("lab1" q) = result ->
value ("lab2" q) - value q1 * value q2 <= 0x1.p-52
goal G3 : forall q:double. ([@lab1] q) = result ->
value ([@lab2] q) - value q1 * value q2 <= 0x1.p-52
end
......
......@@ -13,9 +13,9 @@ module M1
use import int.Int
let f (x "model:0":int) : int
ensures { "model:post" result <= 50 }
= if ("model:cond" x >= 42) then x + 3 else 0
let f (x [@model:0]:int) : int
ensures { [@model:post] result <= 50 }
= if ([@model:cond] x >= 42) then x + 3 else 0
let f_no_lab (x:int) : int
ensures { result <= 50 }
......
......@@ -5,15 +5,15 @@ theory T
goal g_no_lab : forall x:int. x >= 42 -> x + 3 <= 50
goal g_lab0 : forall x "model:0":int. ("model:cond" x >= 42) ->
("model:concl" x + 3 <= 50)
goal g_lab0 : forall x [@model:0]:int. ([@model:cond] x >= 42) ->
([@model:concl] x + 3 <= 50)
goal g_lab1 : forall x "model:1":int. ("model:cond" x >= 42) ->
("model:concl" x + 3 <= 50)
goal g_lab1 : forall x [@model:1]:int. ([@model:cond] x >= 42) ->
([@model:concl] x + 3 <= 50)
constant g : int
goal g2_lab : forall x "model:0":int. ("model:concl" g >= x)
goal g2_lab : forall x [@model:0]:int. ([@model:concl] g >= x)
end
......@@ -22,49 +22,49 @@ theory ModelInt
use import int.Int
goal test0 : forall x "model:0":int. not (0 < x < 1)
goal test0 : forall x [@model:0]:int. not (0 < x < 1)
goal test1 : forall x "model:0":int. not (0 <= x <= 1)
goal test1 : forall x [@model:0]:int. not (0 <= x <= 1)
use import int.EuclideanDivision
goal test2 : forall x "model:0":int. div x x = 1
goal test2 : forall x [@model:0]:int. div x x = 1
goal test_overflow:
forall x "model:0" y "model:0" : int.
forall x [@model:0] y [@model:0] : int.
0 <= x <= 65535 /\ 0 <= y <= 65535 -> 0 <= x + y <= 65535
goal test_overflow2:
forall x "model:0" y "model:0" : int.
forall x [@model:0] y [@model:0] : int.
-2 <= x <= 65535 /\ -2 <= y <= 65535 -> -2 <= x + y <= 65535
predicate is_int16 (x:int) = -65536 <= x <= 65535
goal test_overflow_int16:
forall x "model:0" y "model:0" : int.
forall x [@model:0] y [@model:0] : int.
is_int16 x /\ is_int16 y -> is_int16 (x + y)
goal test_overflow_int16_alt:
forall x "model:0" y "model:0" : int.
forall x [@model:0] y [@model:0] : int.
-65536 <= x <= 65535 /\ -65536 <= y <= 65535 -> -65536 <= x+y <= 65535
goal test_overflow_int16_bis:
forall x "model:0" y "model:0" : int.
forall x [@model:0] y [@model:0] : int.
is_int16 x /\ is_int16 y /\
("model:cond1" 0 <= x) /\ (x <= y) -> is_int16 (x + y)
([@model:cond1] 0 <= x) /\ (x <= y) -> is_int16 (x + y)
predicate is_int32 (x:int) = -2147483648 <= x <= 2147483647
goal test_overflow_int32:
forall x "model:0" y "model:0" : int.
forall x [@model:0] y [@model:0] : int.
is_int32 x /\ is_int32 y -> is_int32 (x + y)
goal test_overflow_int32_bis:
forall x "model:0" y "model:0" : int.
forall x [@model:0] y [@model:0] : int.
is_int32 x /\ is_int32 y /\ 0 <= x <= y -> is_int32 (x + y)
goal test_overflow_int32_bis_inline:
forall x "model:0" y "model:0" : int.
forall x [@model:0] y [@model:0] : int.
-2147483648 <= x <= 2147483647 /\ -2147483648 <= y <= 2147483647 /\ 0 <= x <= y -> -2147483648 <= x + y <= 2147483647
end
......@@ -73,9 +73,9 @@ theory ModelReal
use import real.Real
goal test1 : forall x "model:0":real. not (0.0 < x < 1.0)
goal test1 : forall x [@model:0]:real. not (0.0 < x < 1.0)
goal test2 : forall x "model:0":real. x/x=1.0
goal test2 : forall x [@model:0]:real. x/x=1.0
end
......@@ -83,7 +83,7 @@ theory ModelArray
use import map.Map
goal t1 : forall t "model:0" :map int int, i "model:0" : int.
goal t1 : forall t [@model:0] :map int int, i [@model:0] : int.
get (set t 0 42) i = get t i
end
......
......@@ -5,33 +5,33 @@ module M
type int_type = Integer int
goal G : forall x "model" : int_type. match x with Integer y -> y > 0 end
goal G : forall x [@model] : int_type. match x with Integer y -> y > 0 end
let test_post (x "model" "model_trace:x" : int) (y "model" "model_trace:y" : ref int): unit
ensures { "model_vc_post" old !y >= x }
let test_post (x [@model] [@model_trace:x] : int) (y [@model] [@model_trace:y] : ref int): unit
ensures { [@model_vc_post] old !y >= x }
=
y := x - 1 + !y
(**********************************************************
** Getting counterexamples for terms of primitive types **
**********************************************************)
val y "model" "model_trace:y" :ref int
val y [@model] [@model_trace:y] :ref int
let incr ( x23 "model" "model_trace:x23" : ref int ): unit
ensures { "model_vc_post" !x23 = old !x23 + 2 + !y }
let incr ( x23 [@model] [@model_trace:x23] : ref int ): unit
ensures { [@model_vc_post] !x23 = old !x23 + 2 + !y }
=
(*#"/home/cmarche/recherche/why/tests/c/binary_search.c" 62 27 32#*)
y := !y + 1;
x23 := !x23 + 1;
x23 := !x23 + 1
let test_loop ( x "model" "model_trace:x" : ref int ): unit
ensures { "model_vc_post" !x < old !x }
let test_loop ( x [@model] [@model_trace:x] : ref int ): unit
ensures { [@model_vc_post] !x < old !x }
=
incr x;
label M in
while !x > 0 do
invariant { "model_vc" !x > old !x + (!x at M) }
invariant { [@model_vc] !x > old !x + (!x at M) }
variant { !x }
x := !x - 1
done
......@@ -47,19 +47,19 @@ module M
val map_set (m: map int 'a) (i: int) (v: 'a) : map int 'a
ensures { result = Map.set m i v }
let test_map (x "model" : ref (map int int)) : unit
ensures { "model_vc" !x[0] <> !x[1] }
let test_map (x [@model] : ref (map int int)) : unit
ensures { [@model_vc] !x[0] <> !x[1] }
=
x := map_set !x 0 3
(* Multi-dimensional maps *)
let test_map_multidim1 (x "model" : ref (map int (map int int))) : unit
ensures { "model_vc" !x[0][0] <> !x[1][1] }