Commit 11598d2b authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

simplify copyright headers

+ create AUTHORS file
+ fix the linking exception in LICENSE
+ update the "About" in IDE
+ remove the trailing whitespace
+ inflate my scores at Ohloh
parent ecc1e64d
The Why3 Verification Platform is developed by
François Bobot
Jean-Christophe Filliâtre
Claude Marché
Guillaume Melquiond
Andrei Paskevich
with contributions of
Sylvie Boldo
Simon Cruanes
Leon Gondelman
Johannes Kanig
David Mentré
Benjamin Monate
Thi-Minh-Tuyen Nguyen
Simão Melo de Sousa
Asma Tafat-Bouzid
The Library is distributed under the terms of the GNU Library General The Library is distributed under the terms of the GNU Lesser General
Public License version 2.1 (included below). Public License version 2.1 (included below).
As a special exception to the GNU Library General Public License, you As a special exception to the GNU Lesser General Public License, you
may link, statically or dynamically, a "work that uses the Library" may link, statically or dynamically, a "work that uses the Library"
with a publicly distributed version of the Library to produce an with a publicly distributed version of the Library to produce an
executable file containing portions of the Library, and distribute executable file containing portions of the Library, and distribute that
that executable file under terms of your choice, without any of the executable file under terms of your choice, without any of the additional
additional requirements listed in clause 6 of the GNU Library General requirements listed in clause 6 of the GNU Lesser General Public License.
Public License. By "a publicly distributed version of the Library", we By "a publicly distributed version of the Library", we mean either the
mean either the unmodified Library as distributed, or a unmodified Library as distributed by the authors, or a modified version
modified version of the Library that is distributed under the of the Library that is distributed under the conditions defined in clause
conditions defined in clause 3 of the GNU Library General Public 3 of the GNU Lesser General Public License. This exception does not
License. This exception does not however invalidate any other reasons however invalidate any other reasons why the executable file might be
why the executable file might be covered by the GNU Library General covered by the GNU Lesser General Public License.
Public License.
====================================================================== ======================================================================
......
########################################################################## ####################################################################
# # # #
# Copyright (C) 2010-2012 # # The Why3 Verification Platform / The Why3 Development Team #
# François Bobot # # Copyright 2010-2012 -- INRIA - CNRS - Paris-Sud University #
# Jean-Christophe Filliâtre # # #
# Claude Marché # # This software is distributed under the terms of the GNU Lesser #
# Guillaume Melquiond # # General Public License version 2.1, with the special exception #
# Andrei Paskevich # # on linking described in file LICENSE. #
# # # #
# This software is free software; you can redistribute it and/or # ####################################################################
# modify it under the terms of the GNU Library General Public #
# License version 2.1, with the special exception on linking #
# described in file LICENSE. #
# #
# This software is distributed in the hope that it will be useful, #
# but WITHOUT ANY WARRANTY; without even the implied warranty of #
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. #
# #
##########################################################################
include Version include Version
...@@ -1525,20 +1516,6 @@ headers: ...@@ -1525,20 +1516,6 @@ headers:
headache -c misc/headache_config.txt -h misc/header.txt \ headache -c misc/headache_config.txt -h misc/header.txt \
Makefile.in configure.in src/*.ml* src/*/*.ml* \ Makefile.in configure.in src/*.ml* src/*/*.ml* \
plugins/*/*.ml* src/tools/cpulimit.c plugins/*/*.ml* src/tools/cpulimit.c
headache -c misc/headache_config.txt -h misc/header_gm.txt \
src/transform/abstraction.ml* \
src/transform/instantiate_predicate.ml* \
src/transform/simplify_formula.ml* \
src/printer/print_number.ml* \
src/printer/gappa.ml*
headache -c misc/headache_config.txt -h misc/header_jk.txt \
src/transform/close_epsilon.ml* \
src/transform/lift_epsilon.ml*
headache -c misc/headache_config.txt -h misc/header_sc.txt \
plugins/transform/hypothesis_selection.ml*
sed -i -f misc/fixnames.sed -- \
Makefile.in configure.in src/*.ml* src/*/*.ml* \
plugins/*/*.ml* src/tools/cpulimit.c
######### #########
# myself # myself
......
########################################################################## ####################################################################
# # # #
# Copyright (C) 2010-2012 # # The Why3 Verification Platform / The Why3 Development Team #
# François Bobot # # Copyright 2010-2012 -- INRIA - CNRS - Paris-Sud University #
# Jean-Christophe Filliâtre # # #
# Claude Marché # # This software is distributed under the terms of the GNU Lesser #
# Guillaume Melquiond # # General Public License version 2.1, with the special exception #
# Andrei Paskevich # # on linking described in file LICENSE. #
# # # #
# This software is free software; you can redistribute it and/or # ####################################################################
# modify it under the terms of the GNU Library General Public #
# License version 2.1, with the special exception on linking #
# described in file LICENSE. #
# #
# This software is distributed in the hope that it will be useful, #
# but WITHOUT ANY WARRANTY; without even the implied warranty of #
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. #
# #
##########################################################################
# #
# autoconf input for Objective Caml programs # autoconf input for Objective Caml programs
......
...@@ -114,24 +114,24 @@ theory DoubleOfInt ...@@ -114,24 +114,24 @@ theory DoubleOfInt
lemma jpxorx_pos: forall x:int. x>=0 -> BV32.nth (BV32.bw_xor j' (BV32.from_int2c x)) 31 = True lemma jpxorx_pos: forall x:int. x>=0 -> BV32.nth (BV32.bw_xor j' (BV32.from_int2c x)) 31 = True
lemma from_int2c_to_nat_sub_pos: lemma from_int2c_to_nat_sub_pos:
forall i:int. 0 <= i <= 31 -> forall i:int. 0 <= i <= 31 ->
forall x:int. 0 <= x < Pow2int.pow2 i -> forall x:int. 0 <= x < Pow2int.pow2 i ->
BV32.to_nat_sub (BV32.from_int2c x) (i-1) 0 = x BV32.to_nat_sub (BV32.from_int2c x) (i-1) 0 = x
lemma lemma1_pos : forall x:int. is_int32 x /\ x >= 0 -> lemma lemma1_pos : forall x:int. is_int32 x /\ x >= 0 ->
BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x
(* case x < 0 *) (* case x < 0 *)
lemma jpxorx_neg: forall x:int. x<0 -> lemma jpxorx_neg: forall x:int. x<0 ->
BV32.nth (BV32.bw_xor j' (BV32.from_int2c x)) 31 = False BV32.nth (BV32.bw_xor j' (BV32.from_int2c x)) 31 = False
lemma from_int2c_to_nat_sub_neg: lemma from_int2c_to_nat_sub_neg:
forall i:int. 0 <= i <= 31 -> forall i:int. 0 <= i <= 31 ->
forall x:int. -Pow2int.pow2 i <= x < 0 -> forall x:int. -Pow2int.pow2 i <= x < 0 ->
BV32.to_nat_sub (BV32.from_int2c x) (i-1) 0 = Pow2int.pow2 i + x BV32.to_nat_sub (BV32.from_int2c x) (i-1) 0 = Pow2int.pow2 i + x
lemma lemma1_neg : forall x:int. is_int32 x /\ x < 0 -> lemma lemma1_neg : forall x:int. is_int32 x /\ x < 0 ->
BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x
(**** old (**** old
...@@ -146,8 +146,8 @@ theory DoubleOfInt ...@@ -146,8 +146,8 @@ theory DoubleOfInt
*) *)
lemma from_int2c_to_nat_sub_gen: lemma from_int2c_to_nat_sub_gen:
forall i:int. 0 <= i <= 30 -> forall i:int. 0 <= i <= 30 ->
forall x:int. 0 <= x < Pow2int.pow2 i -> forall x:int. 0 <= x < Pow2int.pow2 i ->
BV32.to_nat_sub (BV32.from_int2c x) (i-1) 0 = x BV32.to_nat_sub (BV32.from_int2c x) (i-1) 0 = x
lemma from_int2c_to_nat_sub: lemma from_int2c_to_nat_sub:
...@@ -181,14 +181,14 @@ theory DoubleOfInt ...@@ -181,14 +181,14 @@ theory DoubleOfInt
BV64.nth (var x) i = BV32.nth (jpxor x) i BV64.nth (var x) i = BV32.nth (jpxor x) i
lemma to_nat_bv32_bv64_aux: forall b1:BV32.bv. forall b2:BV32.bv. forall j:int. 0<=j<32-> BV64.to_nat_sub (BV32_64.concat b1 b2) j 0 = BV32.to_nat_sub b2 j 0 lemma to_nat_bv32_bv64_aux: forall b1:BV32.bv. forall b2:BV32.bv. forall j:int. 0<=j<32-> BV64.to_nat_sub (BV32_64.concat b1 b2) j 0 = BV32.to_nat_sub b2 j 0
lemma to_nat_bv32_bv64: forall b1:BV32.bv. forall b2:BV32.bv. BV64.to_nat_sub (BV32_64.concat b1 b2) 31 0 = BV32.to_nat_sub b2 31 0 lemma to_nat_bv32_bv64: forall b1:BV32.bv. forall b2:BV32.bv. BV64.to_nat_sub (BV32_64.concat b1 b2) 31 0 = BV32.to_nat_sub b2 31 0
lemma to_nat_var_0_31: forall x:int. is_int32(x) -> lemma to_nat_var_0_31: forall x:int. is_int32(x) ->
BV64.to_nat_sub (var x) 31 0 = BV32.to_nat_sub (jpxor x) 31 0 BV64.to_nat_sub (var x) 31 0 = BV32.to_nat_sub (jpxor x) 31 0
lemma nth_var32to63: lemma nth_var32to63:
forall x k:int. 32 <= k <= 63 -> BV64.nth (var x) k = BV32.nth j (k - 32) forall x k:int. 32 <= k <= 63 -> BV64.nth (var x) k = BV32.nth j (k - 32)
lemma nth_var3: forall x:int. forall i:int. 32 <= i <= 51 -> BV64.nth (var x) i = False lemma nth_var3: forall x:int. forall i:int. 32 <= i <= 51 -> BV64.nth (var x) i = False
lemma lemma2 : forall x:int. is_int32 x -> mantissa(var(x)) = Pow2int.pow2 31 + x lemma lemma2 : forall x:int. is_int32 x -> mantissa(var(x)) = Pow2int.pow2 31 + x
(*********************************************************************) (*********************************************************************)
......
theory Stmt "some_statement" theory Stmt "some_statement"
use import real.Real use import real.Real
use import floating_point.Rounding use import floating_point.Rounding
use import floating_point.Single use import floating_point.Single
......
theory T theory T
type t 'a = A 'a | B type t 'a = A 'a | B
function f () : () function f () : ()
goal g : () = f () goal g : () = f ()
......
...@@ -14,7 +14,7 @@ theory Th2 ...@@ -14,7 +14,7 @@ theory Th2
goal foo : false goal foo : false
end end
theory Th3 theory Th3
......
...@@ -23,7 +23,7 @@ theory Einstein "Einstein's problem" ...@@ -23,7 +23,7 @@ theory Einstein "Einstein's problem"
type drink = Beer | Coffee | Milk | Tea | Water type drink = Beer | Coffee | Milk | Tea | Water
type cigar = Blend | BlueMaster | Dunhill | PallMall | Prince type cigar = Blend | BlueMaster | Dunhill | PallMall | Prince
type pet = Birds | Cats | Dogs | Fish | Horse type pet = Birds | Cats | Dogs | Fish | Horse
(* Each house is associated bijectively to a color and a person *) (* Each house is associated bijectively to a color and a person *)
clone Bijection as Color with type t = house, type u = color clone Bijection as Color with type t = house, type u = color
clone Bijection as Owner with type t = house, type u = person clone Bijection as Owner with type t = house, type u = person
...@@ -36,9 +36,9 @@ theory Einstein "Einstein's problem" ...@@ -36,9 +36,9 @@ theory Einstein "Einstein's problem"
(* Relative positions of the houses *) (* Relative positions of the houses *)
predicate leftof (h1 h2 : house) = predicate leftof (h1 h2 : house) =
match h1, h2 with match h1, h2 with
| H1, H2 | H1, H2
| H2, H3 | H2, H3
| H3, H4 | H3, H4
| H4, H5 -> true | H4, H5 -> true
| _ -> false | _ -> false
end end
...@@ -79,7 +79,7 @@ theory EinsteinClues "Clues" ...@@ -79,7 +79,7 @@ theory EinsteinClues "Clues"
axiom Clue9: Owner.of H1 = Norwegian axiom Clue9: Owner.of H1 = Norwegian
(* The man who smokes Blends lives next to the one who has cats *) (* The man who smokes Blends lives next to the one who has cats *)
axiom Clue10: neighbour axiom Clue10: neighbour
(Owner.to_ (Cigar.to_ Blend)) (Owner.to_ (Pet.to_ Cats)) (Owner.to_ (Cigar.to_ Blend)) (Owner.to_ (Pet.to_ Cats))
(* The man who owns a horse lives next to the one who smokes Dunhills *) (* The man who owns a horse lives next to the one who smokes Dunhills *)
...@@ -123,13 +123,13 @@ theory Goals "Goals about Einstein's problem" ...@@ -123,13 +123,13 @@ theory Goals "Goals about Einstein's problem"
lemma Yellow_H1 : Color.of H1 = Yellow lemma Yellow_H1 : Color.of H1 = Yellow
*) *)
goal G1: Pet.to_ Fish = German goal G1: Pet.to_ Fish = German
goal Wrong: Pet.to_ Cats = Swede goal Wrong: Pet.to_ Cats = Swede
goal G2: Pet.to_ Cats = Norwegian goal G2: Pet.to_ Cats = Norwegian
end end
(* (*
Local Variables: Local Variables:
compile-command: "make -C .. examples/einstein.gui" compile-command: "make -C .. examples/einstein.gui"
End: End:
*) *)
...@@ -4,7 +4,7 @@ theory Genealogy ...@@ -4,7 +4,7 @@ theory Genealogy
type person type person
type gender = Male | Female type gender = Male | Female
function gender person : gender function gender person : gender
function father person : person function father person : person
...@@ -20,7 +20,7 @@ theory Genealogy ...@@ -20,7 +20,7 @@ theory Genealogy
predicate child (c : person) (p : person) = parent p c predicate child (c : person) (p : person) = parent p c
goal Child_is_son_or_daughter: goal Child_is_son_or_daughter:
forall c p : person. child c p <-> son c p \/ daughter c p forall c p : person. child c p <-> son c p \/ daughter c p
predicate sibling (p1 : person) (p2 : person) = predicate sibling (p1 : person) (p2 : person) =
...@@ -45,14 +45,14 @@ theory Genealogy ...@@ -45,14 +45,14 @@ theory Genealogy
goal Grandparent_is_grandfather_or_grandmother: goal Grandparent_is_grandfather_or_grandmother:
forall g p : person. grandparent g p <-> grandfather g p \/ grandmother g p forall g p : person. grandparent g p <-> grandfather g p \/ grandmother g p
goal Grandfather_male: goal Grandfather_male:
forall g p : person. grandfather g p -> gender g = Male forall g p : person. grandfather g p -> gender g = Male
goal Grandmother_female: goal Grandmother_female:
forall g p : person. grandmother g p -> gender g = Female forall g p : person. grandmother g p -> gender g = Female
goal Only_two_grandfathers: goal Only_two_grandfathers:
forall g1 g2 g3 p : person. forall g1 g2 g3 p : person.
grandfather g1 p -> grandfather g1 p ->
grandfather g2 p -> grandfather g2 p ->
grandfather g3 p -> grandfather g3 p ->
(g1 = g2 \/ g2 = g3 \/ g1 = g3) (g1 = g2 \/ g2 = g3 \/ g1 = g3)
......
...@@ -18,9 +18,9 @@ type value = Vvoid | Vint int | Vbool bool ...@@ -18,9 +18,9 @@ type value = Vvoid | Vint int | Vbool bool
type operator = Oplus | Ominus | Omult | Ole type operator = Oplus | Ominus | Omult | Ole
(** ident for imutable variable*) (** ident for imutable variable*)
type ident type ident
constant result : ident constant result : ident
type term = type term =
| Tvalue value | Tvalue value
...@@ -86,13 +86,13 @@ predicate eval_fmla (sigma:env) (pi:stack) (f:fmla) = ...@@ -86,13 +86,13 @@ predicate eval_fmla (sigma:env) (pi:stack) (f:fmla) =
| Fand f1 f2 -> eval_fmla sigma pi f1 /\ eval_fmla sigma pi f2 | Fand f1 f2 -> eval_fmla sigma pi f1 /\ eval_fmla sigma pi f2
| Fnot f -> not (eval_fmla sigma pi f) | Fnot f -> not (eval_fmla sigma pi f)
| Fimplies f1 f2 -> eval_fmla sigma pi f1 -> eval_fmla sigma pi f2 | Fimplies f1 f2 -> eval_fmla sigma pi f1 -> eval_fmla sigma pi f2
| Flet x t f -> | Flet x t f ->
eval_fmla sigma (Cons (x,eval_term sigma pi t) pi) f eval_fmla sigma (Cons (x,eval_term sigma pi t) pi) f
| Fforall x TYint f -> | Fforall x TYint f ->
forall n:int. eval_fmla sigma (Cons (x,Vint n) pi) f forall n:int. eval_fmla sigma (Cons (x,Vint n) pi) f
| Fforall x TYbool f -> | Fforall x TYbool f ->
forall b:bool. eval_fmla sigma (Cons (x,Vbool b) pi) f forall b:bool. eval_fmla sigma (Cons (x,Vbool b) pi) f
| Fforall x TYunit f -> eval_fmla sigma (Cons (x,Vvoid) pi) f | Fforall x TYunit f -> eval_fmla sigma (Cons (x,Vvoid) pi) f
end end
(** substitution of a reference [r] by a logic variable [v] (** substitution of a reference [r] by a logic variable [v]
......
...@@ -171,7 +171,7 @@ inductive type_expr type_env type_stack expr datatype = ...@@ -171,7 +171,7 @@ inductive type_expr type_env type_stack expr datatype =
type_expr sigma pi e1 TYbool -> type_expr sigma pi e1 TYbool ->
type_expr sigma pi e2 ty -> type_expr sigma pi e2 ty ->
type_expr sigma pi e3 ty -> type_expr sigma pi e3 ty ->
type_expr sigma pi (Eif e1 e2 e3) ty type_expr sigma pi (Eif e1 e2 e3) ty
| Type_eassert : | Type_eassert :
forall sigma: type_env, pi:type_stack, p:fmla. forall sigma: type_env, pi:type_stack, p:fmla.
type_fmla sigma pi p -> type_fmla sigma pi p ->
...@@ -372,7 +372,7 @@ lemma let_implies : ...@@ -372,7 +372,7 @@ lemma let_implies :
forall id:ident, t:term, p q:fmla. forall id:ident, t:term, p q:fmla.
valid_fmla (Fimplies p q) -> valid_fmla (Fimplies p q) ->
valid_fmla (Fimplies (Flet id t p) (Flet id t q)) valid_fmla (Fimplies (Flet id t p) (Flet id t q))
predicate fresh_in_expr (id:ident) (e:expr) = predicate fresh_in_expr (id:ident) (e:expr) =
match e with match e with
| Evalue _ -> true | Evalue _ -> true
...@@ -652,12 +652,12 @@ end ...@@ -652,12 +652,12 @@ end
theory Simpl_tautology theory Simpl_tautology
predicate p predicate p
predicate q predicate q
lemma simpl_tautology : lemma simpl_tautology :
(p -> q) <-> (p /\ q <-> p) (p -> q) <-> (p /\ q <-> p)
end end
(** {2 WP calculus} *) (** {2 WP calculus} *)
...@@ -792,17 +792,17 @@ predicate expr_writes (e:expr) (w:Set.set mident) = ...@@ -792,17 +792,17 @@ predicate expr_writes (e:expr) (w:Set.set mident) =
forall e:expr. not (is_value e) \/ exists v:value. e = Evalue v forall e:expr. not (is_value e) \/ exists v:value. e = Evalue v
lemma bool_value: lemma bool_value:
forall v:value, sigmat: type_env, pit:type_stack. forall v:value, sigmat: type_env, pit:type_stack.
type_expr sigmat pit (Evalue v) TYbool -> type_expr sigmat pit (Evalue v) TYbool ->
(v = Vbool False) \/ (v = Vbool True) (v = Vbool False) \/ (v = Vbool True)
lemma unit_value: lemma unit_value:
forall v:value, sigmat: type_env, pit:type_stack. forall v:value, sigmat: type_env, pit:type_stack.
type_expr sigmat pit (Evalue v) TYunit -> v = Vvoid type_expr sigmat pit (Evalue v) TYunit -> v = Vvoid
lemma progress: lemma progress:
forall e:expr, sigma:env, pi:stack, sigmat: type_env, pit: type_stack, ty: datatype, q:fmla. forall e:expr, sigma:env, pi:stack, sigmat: type_env, pit: type_stack, ty: datatype, q:fmla.
type_expr sigmat pit e ty -> type_expr sigmat pit e ty ->
type_fmla sigmat (Cons(result, ty) pit) q -> type_fmla sigmat (Cons(result, ty) pit) q ->
eval_fmla sigma pi (wp e q) -> not is_value e -> eval_fmla sigma pi (wp e q) -> not is_value e ->
exists sigma':env, pi':stack, e':expr. exists sigma':env, pi':stack, e':expr.
......
...@@ -806,7 +806,7 @@ predicate stmt_writes (s:stmt) (w:Set.set mident) = ...@@ -806,7 +806,7 @@ predicate stmt_writes (s:stmt) (w:Set.set mident) =
sigma,pi |= (wp s p) -> (wp s q) sigma,pi |= (wp s p) -> (wp s q)
meme contre-exemple: sigma(x) = 42 alors true -> x=42 meme contre-exemple: sigma(x) = 42 alors true -> x=42
mais mais
wp (x := 7) true = true wp (x := 7) true = true
wp (x := 7) x=42 = 7=42 wp (x := 7) x=42 = 7=42
*) *)
......
...@@ -30,7 +30,7 @@ axiom mident_decide : ...@@ -30,7 +30,7 @@ axiom mident_decide :
(** ident for immutable variables *) (** ident for immutable variables *)
type ident = { ident_index : int } type ident = { ident_index : int }
constant result : ident constant result : ident
axiom ident_decide : axiom ident_decide :
...@@ -134,7 +134,7 @@ function get_vartype (i:ident) (pi:type_stack) : datatype = ...@@ -134,7 +134,7 @@ function get_vartype (i:ident) (pi:type_stack) : datatype =
| Cons (x,ty) r -> if x=i then ty else get_vartype i r | Cons (x,ty) r -> if x=i then ty else get_vartype i r
end end
type type_env = IdMap.map mident datatype (* map global mutable variables to their type *) type type_env = IdMap.map mident datatype (* map global mutable variables to their type *)
function get_reftype (i:mident) (e:type_env) : datatype = IdMap.get e i function get_reftype (i:mident) (e:type_env) : datatype = IdMap.get e i
...@@ -335,7 +335,7 @@ function msubst_term (t:term) (r:mident) (v:ident) : term = ...@@ -335,7 +335,7 @@ function msubst_term (t:term) (r:mident) (v:ident) : term =
| Tvalue _ | Tvar _ -> t | Tvalue _ | Tvar _ -> t
| Tderef x -> if r = x then mk_tvar v else t | Tderef x -> if r = x then mk_tvar v else t
| Tbin t1 op t2 -> | Tbin t1 op t2 ->
mk_tbin (msubst_term t1 r v) op (msubst_term t2 r v) mk_tbin (msubst_term t1 r v) op (msubst_term t2 r v)
end end
function subst_term (t:term) (r:ident) (v:ident) : term = function subst_term (t:term) (r:ident) (v:ident) : term =
...@@ -359,7 +359,7 @@ lemma fresh_in_binop: ...@@ -359,7 +359,7 @@ lemma fresh_in_binop:
forall t t':term, op:operator, v:ident. forall t t':term, op:operator, v:ident.
fresh_in_term v (mk_tbin t op t') -> fresh_in_term v (mk_tbin t op t') ->
fresh_in_term v t /\ fresh_in_term v t' fresh_in_term v t /\ fresh_in_term v t'
(* lemma eval_subst_term: *) (* lemma eval_subst_term: *)
(* forall sigma:env, pi:stack, e:term, x:ident, v:ident. *) (* forall sigma:env, pi:stack, e:term, x:ident, v:ident. *)
(* fresh_in_term v e -> *) (* fresh_in_term v e -> *)
...@@ -506,10 +506,10 @@ predicate fresh_in_expr (id:ident) (e:expr) = ...@@ -506,10 +506,10 @@ predicate fresh_in_expr (id:ident) (e:expr) =
match e with match e with
| Evalue _ -> true | Evalue _ -> true
| Ebin e1 op e2 -> fresh_in_expr id e1 /\ fresh_in_expr id e2 | Ebin e1 op e2 -> fresh_in_expr id e1 /\ fresh_in_expr id e2
| Evar v -> id <> v | Evar v -> id <> v
| Ederef _ -> true | Ederef _ -> true
| Eassign x e -> fresh_in_expr id e | Eassign x e -> fresh_in_expr id e
| Eseq e1 e2 -> fresh_in_expr id e1 /\ fresh_in_expr id e2 | Eseq e1 e2 -> fresh_in_expr id e1 /\ fresh_in_expr id e2
| Elet v e1 e2 -> id <> v /\ fresh_in_expr id e1 /\ fresh_in_expr id e2 | Elet v e1 e2 -> id <> v /\ fresh_in_expr id e1 /\ fresh_in_expr id e2
| Eif e1 e2 e3 -> fresh_in_expr id e1 /\ fresh_in_expr id e2 /\ fresh_in_expr id e3 | Eif e1 e2 e3 -> fresh_in_expr id e1 /\ fresh_in_expr id e2 /\ fresh_in_expr id e3
| Eassert f -> fresh_in_fmla id f | Eassert f -> fresh_in_fmla id f
...@@ -889,7 +889,7 @@ predicate expr_writes (s:expr) (w:Set.set mident) = ...@@ -889,7 +889,7 @@ predicate expr_writes (s:expr) (w:Set.set mident) =
forall s:expr, sigma:env, pi:stack, p q:fmla. forall s:expr, sigma:env, pi:stack, p q:fmla.
(eval_fmla sigma pi (wp s p)) /\ (eval_fmla sigma pi (wp s p)) /\
(eval_fmla sigma pi (wp s q)) -> (eval_fmla sigma pi (wp s q)) ->
eval_fmla sigma pi (wp s (Fand p q)) eval_fmla sigma pi (wp s (Fand p q))
lemma wp_reduction: lemma wp_reduction:
forall sigma sigma':env, pi pi':stack, s s':expr. forall sigma sigma':env, pi pi':stack, s s':expr.
...@@ -908,20 +908,20 @@ predicate expr_writes (s:expr) (w:Set.set mident) = ...@@ -908,20 +908,20 @@ predicate expr_writes (s:expr) (w:Set.set mident) =
forall e:expr. not (is_value e) \/ exists v:value. e = Evalue v forall e:expr. not (is_value e) \/ exists v:value. e = Evalue v
lemma bool_value: lemma bool_value:
forall v:value, sigmat: type_env, pit:type_stack. forall v:value, sigmat: type_env, pit:type_stack.
type_expr sigmat pit (Evalue v) TYbool -> type_expr sigmat pit (Evalue v) TYbool ->
(v = Vbool False) \/ (v = Vbool True) (v = Vbool False) \/ (v = Vbool True)
lemma unit_value: lemma unit_value:
forall v:value, sigmat: type_env, pit:type_stack. forall v:value, sigmat: type_env, pit:type_stack.
type_expr sigmat pit (Evalue v) TYunit -> v = Vvoid type_expr sigmat pit (Evalue v) TYunit -> v = Vvoid
lemma progress: lemma progress: