From 02d7ec75988e2cd13ebf233b364e400309c605a3 Mon Sep 17 00:00:00 2001
From: filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 29 Mar 2001 14:27:11 +0000
Subject: mise en place de Correctness (ne compile pas encore)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1501 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/correctness/pwp.ml | 342 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 342 insertions(+)
 create mode 100644 contrib/correctness/pwp.ml

(limited to 'contrib/correctness/pwp.ml')

diff --git a/contrib/correctness/pwp.ml b/contrib/correctness/pwp.ml
new file mode 100644
index 000000000..af6801a1c
--- /dev/null
+++ b/contrib/correctness/pwp.ml
@@ -0,0 +1,342 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* Certification of Imperative Programs / Jean-Christophe Filliātre *)
+
+(* $Id$ *)
+
+open More_util
+open Names
+open Generic
+open Term
+open Environ
+
+open Pmisc
+open Ptype
+open Past
+open Putil
+open Penv
+open Peffect
+open Ptyping
+open Prename
+
+(* In this module:
+ *  - we try to insert more annotations to achieve a greater completeness;
+ *  - we recursively propagate annotations inside programs;
+ *  - we normalize boolean expressions.
+ *
+ * The propagation schemas are the following:
+ * 
+ *  1. (f a1 ... an)  ->  (f a1 ... an) {Qf} if the ai are functional
+ *
+ *  2. (if e1 then e2 else e3) {Q}  ->  (if e1 then e2 {Q} else e3 {Q}) {Q}
+ * 
+ *  3. (let x = e1 in e2) {Q}  ->  (let x = e1 in e2 {Q}) {Q}
+ *)
+
+(* force a post-condition *)
+let update_post env top ef c =
+  let i,o = Effects.get_repr ef in
+  let al = 
+    List.fold_left 
+      (fun l id -> 
+	 if is_mutable_in_env env id then
+	   if is_write ef id then l else (id,at_id id "")::l
+	 else if is_at id then
+	   let (uid,d) = un_at id in
+	   if is_mutable_in_env env uid & d="" then 
+	     (id,at_id uid top)::l 
+	   else 
+	     l
+	 else
+	   l) 
+      [] (global_vars c)
+  in
+  subst_in_constr al c
+  
+let force_post up env top q e =
+  let (res,ef,p,_) = e.info.kappa in
+  let q' = 
+    if up then option_app (named_app (update_post env top ef)) q else q 
+  in
+  let i = { env = e.info.env; kappa = (res,ef,p,q') } in
+  { desc = e.desc; pre = e.pre; post = q'; loc = e.loc; info = i }
+
+(* put a post-condition if none is present *)
+let post_if_none_up env top q = function
+    { post = None } as p -> force_post true env top q p 
+  | p -> p
+
+let post_if_none env q = function
+    { post = None } as p -> force_post false env "" q p 
+  | p -> p
+
+(* [annotation_candidate p] determines if p is a candidate for a 
+ * post-condition *)
+
+let annotation_candidate = function
+    { desc = If _ | LetIn _ | LetRef _ ; post = None } -> true
+  | _ -> false
+
+(* [extract_pre p] erase the pre-condition of p and returns it *)
+let extract_pre pr =
+  let (v,e,p,q) = pr.info.kappa in
+  { desc = pr.desc; pre = []; post = pr.post; loc = pr.loc;
+    info = { env = pr.info.env; kappa = (v,e,[],q) } },
+  p
+
+(* adds some pre-conditions *)
+let add_pre p1 pr =
+  let (v,e,p,q) = pr.info.kappa in
+  let p' = p1 @ p in
+  { desc = pr.desc; pre = p'; post = pr.post; loc = pr.loc;
+    info = { env = pr.info.env; kappa = (v,e,p',q) } }
+  
+(* change the statement *)
+let change_desc p d =
+  { desc = d; pre = p.pre; post = p.post; loc = p.loc; info = p.info }
+
+let create_bool_post c =
+  Some { a_value = c; a_name = Name (bool_name()) }
+
+(* [normalize_boolean b] checks if the boolean expression b (of type bool) is 
+ * annotated, and if it is not the case tries to add the annotation
+ * (if result then c=true else c=false) if b is an expression c.
+ *)
+
+let bool_id = id_of_string "bool"
+
+let is_bool = function
+    TypePure c ->
+      (match (strip_outer_cast c) with
+	   DOPN(MutInd _ as op,_) -> id_of_global op = bool_id
+	 | _ -> false)
+  | _ -> false
+
+let normalize_boolean ren env b =
+  let ((res,v),ef,p,q) = b.info.kappa in
+  Prog_errors.check_no_effect b.loc ef;
+  if is_bool v then
+    match q with
+	Some _ ->
+	  (* il y a une annotation : on se contente de lui forcer un nom *)
+	  let q = force_bool_name q in
+	  { desc = b.desc; pre = b.pre; post = q; loc = b.loc;
+	    info = { env = b.info.env; kappa = ((res,v),ef,p,q) } }
+      | None -> begin
+	  (* il n'y a pas d'annotation : on cherche ą en mettre une *)
+	  match b.desc with
+	      Expression c ->
+	    	let c' = Term.applist (constant "annot_bool",[c]) in
+		let ty = type_of_expression ren env c' in
+		let (_,q') = dest_sig ty in
+		let q' = Some { a_value = q'; a_name = Name (bool_name()) } in
+		{ desc = Expression c'; 
+		  pre = b.pre; post = q'; loc = b.loc;
+		  info = { env = b.info.env; kappa = ((res, v),ef,p,q') } }
+	    | _ -> b
+	end
+  else
+    Prog_errors.should_be_boolean b.loc
+
+(* [decomp_boolean c] returns the specs R and S of a boolean expression *)
+
+let decomp_boolean = function
+    Some { a_value = q } ->
+      Reduction.whd_betaiota (Term.applist (q, [constant "true"])),
+      Reduction.whd_betaiota (Term.applist (q, [constant "false"]))
+  | _ -> invalid_arg "Prog_typing.decomp_boolean"
+
+(* top point of a program *)
+
+let top_point = function
+    PPoint (s,_) as p -> s,p
+  | p -> let s = label_name() in s,PPoint(s,p)
+
+let top_point_block = function
+    (Label s :: _) as b -> s,b
+  | b -> let s = label_name() in s,(Label s)::b
+
+let abstract_unit q = abstract [result_id,constant "unit"] q
+
+(* [add_decreasing env ren ren' phi r bl] adds the decreasing condition
+ *    phi(ren') r phi(ren)
+ * to the last assertion of the block [bl], which is created if needed
+ *)
+
+let add_decreasing env inv (var,r) lab bl =
+  let ids = now_vars env var in
+  let al = List.map (fun id -> (id,at_id id lab)) ids in
+  let var_lab = subst_in_constr al var in
+  let dec = Term.applist (r, [var;var_lab]) in
+  let post = match inv with
+      None -> anonymous dec
+    | Some i -> { a_value = conj dec i.a_value; a_name = i.a_name }
+  in
+  bl @ [ Assert post ]
+
+(* [post_last_statement env top q bl] annotates the last statement of the
+ * sequence bl with q if necessary *)
+
+let post_last_statement env top q bl =
+  match List.rev bl with
+      Statement e :: rem when annotation_candidate e -> 
+	List.rev ((Statement (post_if_none_up env top q e)) :: rem)
+    | _ -> bl
+
+(* [propagate_desc] moves the annotations inside the program 
+ * info is the typing information coming from the outside annotations *)
+let rec propagate_desc ren info d = 
+  let env = info.env in
+  let (_,_,p,q) = info.kappa in
+  match d with
+      If (e1,e2,e3) ->
+      (* propagation number 2 *)
+	let e1' = normalize_boolean ren env (propagate ren e1) in
+	if e2.post = None or e3.post = None then
+	  let top = label_name() in
+	  let ren' = push_date ren top in
+	  PPoint (top, If (e1', 
+			   propagate ren' (post_if_none_up env top q e2),
+			   propagate ren' (post_if_none_up env top q e3)))
+	else
+	  If (e1', propagate ren e2, propagate ren e3)
+    | Aff (x,e) ->
+      	Aff (x, propagate ren e)
+    | TabAcc (ch,x,e) ->
+      	TabAcc (ch, x, propagate ren e)
+    | TabAff (ch,x,({desc=Expression c} as e1),e2) ->
+	let p = Monad.make_pre_access ren env x c in
+	let e1' = add_pre [(anonymous_pre true p)] e1 in
+      	TabAff (false, x, propagate ren e1', propagate ren e2)
+    | TabAff (ch,x,e1,e2) ->
+      	TabAff (ch, x, propagate ren e1, propagate ren e2)
+    | App (f,l) ->
+      	App (propagate ren f, List.map (propagate_arg ren) l)
+    | SApp (f,l) ->
+	let l = 
+	  List.map (fun e -> normalize_boolean ren env (propagate ren e)) l
+	in
+      	SApp (f, l)
+    | Lam (bl,e) ->
+      	Lam (bl, propagate ren e)
+    | Seq bl ->
+	let top,bl = top_point_block bl in
+	let bl = post_last_statement env top q bl in
+      	Seq (propagate_block ren env bl)
+    | While (b,inv,var,bl) ->
+	let b = normalize_boolean ren env (propagate ren b) in
+	let lab,bl = top_point_block bl in
+	let bl = add_decreasing env inv var lab bl in
+      	While (b,inv,var,propagate_block ren env bl)
+    | LetRef (x,e1,e2) ->
+	let top = label_name() in
+	let ren' = push_date ren top in
+	PPoint (top, LetRef (x, propagate ren' e1, 
+	      		     propagate ren' (post_if_none_up env top q e2)))
+    | LetIn (x,e1,e2) ->
+	let top = label_name() in
+	let ren' = push_date ren top in
+      	PPoint (top, LetIn (x, propagate ren' e1, 
+			    propagate ren' (post_if_none_up env top q e2)))
+    | LetRec (f,bl,v,var,e) ->
+      	LetRec (f, bl, v, var, propagate ren e)
+    | PPoint (s,d) -> 
+      	PPoint (s, propagate_desc ren info d)
+    | Debug _ | Var _ 
+    | Acc _ | Expression _ as d -> d
+	  
+
+(* [propagate] adds new annotations if possible *)
+and propagate ren p =
+  let env = p.info.env in
+  let p = match p.desc with
+      App (f,l) ->
+	let _,(_,so,ok),(_,_,_,qapp) = effect_app ren env f l in
+	if ok then
+	  let q = option_app (named_app (real_subst_in_constr so)) qapp in
+	  post_if_none env q p
+	else
+	  p
+    | _ -> p
+  in
+  let d = propagate_desc ren p.info p.desc in
+  let p = change_desc p d in
+  match d with
+    | Aff (x,e) ->
+	let e1,p1 = extract_pre e in
+	change_desc (add_pre p1 p) (Aff (x,e1))
+
+    | TabAff (check, x, ({ desc = Expression _ } as e1), e2) ->
+	let e1',p1 = extract_pre e1 in
+	let e2',p2 = extract_pre e2 in
+	change_desc (add_pre (p1@p2) p) (TabAff (check,x,e1',e2'))
+
+    | While (b,inv,_,_) ->
+	let _,s = decomp_boolean b.post in
+	let s = make_before_after s in
+	let q = match inv with
+	    None -> Some (anonymous s)
+	  | Some i -> Some { a_value = conj i.a_value s; a_name = i.a_name }
+	in
+	let q = option_app (named_app abstract_unit) q in
+	post_if_none env q p
+
+    | SApp ([Var id], [e1;e2]) 
+      when id = connective_and or id = connective_or ->
+	let (_,_,_,q1) = e1.info.kappa
+	and (_,_,_,q2) = e2.info.kappa in
+	let (r1,s1) = decomp_boolean q1
+	and (r2,s2) = decomp_boolean q2 in
+	let q =
+	  let conn = if id = connective_and then "spec_and" else "spec_or" in
+	  let c = Term.applist (constant conn, [r1; s1; r2; s2]) in
+	  let c = Reduction.whd_betadeltaiota (Evd.mt_evd()) c in
+	  create_bool_post c
+	in
+	let d = 
+	  SApp ([Var id; Expression (out_post q1); Expression (out_post q2)], 
+		[e1; e2] ) 
+	in
+	post_if_none env q (change_desc p d)
+
+    | SApp ([Var id], [e1]) when id = connective_not ->
+	let (_,_,_,q1) = e1.info.kappa in
+	let (r1,s1) = decomp_boolean q1 in
+	let q = 
+	  let c = Term.applist (constant "spec_not", [r1; s1]) in
+	  let c = Reduction.whd_betadeltaiota (Evd.mt_evd()) c in
+	  create_bool_post c 
+	in
+	let d = SApp ([Var id; Expression (out_post q1)], [ e1 ]) in
+	post_if_none env q (change_desc p d)
+
+    | _ -> p
+
+and propagate_arg ren = function
+    Type _ | Refarg _ as a -> a
+  | Term e -> Term (propagate ren e)
+
+
+and propagate_block ren env = function 
+    [] -> []
+  | (Statement p) :: (Assert q) :: rem when annotation_candidate p ->
+      let q' =
+	let ((id,v),_,_,_) = p.info.kappa in
+	let tv = Monad.trad_ml_type_v ren env v in
+	named_app (abstract [id,tv]) q
+      in
+      let p' = post_if_none env (Some q') p in
+      (Statement (propagate ren p')) :: (Assert q) 
+      :: (propagate_block ren env rem)
+  | (Statement p) :: rem ->
+      (Statement (propagate ren p)) :: (propagate_block ren env rem)
+  | (Label s as x) :: rem ->
+      x :: propagate_block (push_date ren s) env rem
+  | x :: rem ->
+      x :: propagate_block ren env rem
-- 
cgit v1.2.3