From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 contrib/correctness/preuves.v | 128 ------------------------------------------
 1 file changed, 128 deletions(-)
 delete mode 100644 contrib/correctness/preuves.v

(limited to 'contrib/correctness/preuves.v')

diff --git a/contrib/correctness/preuves.v b/contrib/correctness/preuves.v
deleted file mode 100644
index 33659b43..00000000
--- a/contrib/correctness/preuves.v
+++ /dev/null
@@ -1,128 +0,0 @@
-
-(* Quelques preuves sur des programmes simples,
- * juste histoire d'avoir un petit bench.
- *)
-
-Require Correctness.
-Require Omega.
-
-Global Variable x : Z ref.
-Global Variable y : Z ref.
-Global Variable z : Z ref.
-Global Variable i : Z ref.
-Global Variable j : Z ref.
-Global Variable n : Z ref.
-Global Variable m : Z ref.
-Variable r : Z.
-Variable N : Z.
-Global Variable t : array N of Z.
-
-(**********************************************************************)
-
-Require Exchange.
-Require ArrayPermut.
-
-Correctness swap
-  fun (N:Z)(t:array N of Z)(i,j:Z) ->
-    { `0 <= i < N` /\ `0 <= j < N` }
-    (let v = t[i] in
-     begin
-       t[i] := t[j];
-       t[j] := v
-     end)
-    { (exchange t t@ i j) }.
-Proof.
-Auto with datatypes.
-Save.
-
-Correctness downheap
-  let rec downheap (N:Z)(t:array N of Z) : unit { variant `0` } =
-    (swap N t 0 0) { True }
-.
-
-(**********************************************************************)
-
-Global Variable x : Z ref.
-Debug on.
-Correctness assign0 (x := 0) { `x=0` }.
-Save.
-
-(**********************************************************************)
-
-Global Variable i : Z ref.
-Debug on.
-Correctness assign1 { `0 <= i` } (i := !i + 1) { `0 < i` }.
-Omega.
-Save.
-
-(**********************************************************************)
-
-Global Variable i : Z ref.
-Debug on.
-Correctness if0 { `0 <= i` } (if !i>0 then i:=!i-1 else tt) { `0 <= i` }.
-Omega.
-Save.
-
-(**********************************************************************)
-
-Global Variable i : Z ref.
-Debug on.
-Correctness assert0 { `0 <= i` } begin assert { `i=2` }; i:=!i-1 end { `i=1` }.
-
-(**********************************************************************)
-
-Correctness echange
-  { `0 <= i < N` /\ `0 <= j < N` }
-  begin
-    label B;
-    x := t[!i]; t[!i] := t[!j]; t[!j] := !x;
-    assert { #t[i] = #t@B[j] /\ #t[j] = #t@B[i] }
-  end.
-Proof.
-Auto with datatypes.
-Save.
-
-  
-(**********************************************************************)
-
-(*
- *   while x <= y do x := x+1 done { y < x }
- *)
-
-Correctness incrementation
-  while !x < !y do
-    { invariant True variant `(Zs y)-x` }
-    x := !x + 1
-  done
-  { `y < x` }.
-Proof.
-Exact (Zwf_well_founded `0`).
-Unfold Zwf. Omega.
-Exact I.
-Save.
-
-
-(************************************************************************)
-
-Correctness pivot1
-  begin
-    while (Z_lt_ge_dec !i r) do
-      { invariant True variant (Zminus (Zs r) i) } i := (Zs !i)
-    done;
-    while (Z_lt_ge_dec r !j) do
-      { invariant True variant (Zminus (Zs j) r) } j := (Zpred !j)
-    done
-  end
-  { `j <= r` /\ `r <= i` }.
-Proof.
-Exact (Zwf_well_founded `0`).
-Unfold Zwf. Omega.
-Exact I.
-Exact (Zwf_well_founded `0`).
-Unfold Zwf. Unfold Zpred. Omega.
-Exact I.
-Omega.
-Save.
-
-
-
-- 
cgit v1.2.3