← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to contrib/correctness/preuves.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
contrib/correctness/preuves.v
 
1
 
 
2
(* Quelques preuves sur des programmes simples,
 
3
 * juste histoire d'avoir un petit bench.
 
4
 *)
 
5
 
 
6
Require Correctness.
 
7
Require Omega.
 
8
 
 
9
Global Variable x : Z ref.
 
10
Global Variable y : Z ref.
 
11
Global Variable z : Z ref.
 
12
Global Variable i : Z ref.
 
13
Global Variable j : Z ref.
 
14
Global Variable n : Z ref.
 
15
Global Variable m : Z ref.
 
16
Variable r : Z.
 
17
Variable N : Z.
 
18
Global Variable t : array N of Z.
 
19
 
 
20
(**********************************************************************)
 
21
 
 
22
Require Exchange.
 
23
Require ArrayPermut.
 
24
 
 
25
Correctness swap
 
26
  fun (N:Z)(t:array N of Z)(i,j:Z) ->
 
27
    { `0 <= i < N` /\ `0 <= j < N` }
 
28
    (let v = t[i] in
 
29
     begin
 
30
       t[i] := t[j];
 
31
       t[j] := v
 
32
     end)
 
33
    { (exchange t t@ i j) }.
 
34
Proof.
 
35
Auto with datatypes.
 
36
Save.
 
37
 
 
38
Correctness downheap
 
39
  let rec downheap (N:Z)(t:array N of Z) : unit { variant `0` } =
 
40
    (swap N t 0 0) { True }
 
41
.
 
42
 
 
43
(**********************************************************************)
 
44
 
 
45
Global Variable x : Z ref.
 
46
Debug on.
 
47
Correctness assign0 (x := 0) { `x=0` }.
 
48
Save.
 
49
 
 
50
(**********************************************************************)
 
51
 
 
52
Global Variable i : Z ref.
 
53
Debug on.
 
54
Correctness assign1 { `0 <= i` } (i := !i + 1) { `0 < i` }.
 
55
Omega.
 
56
Save.
 
57
 
 
58
(**********************************************************************)
 
59
 
 
60
Global Variable i : Z ref.
 
61
Debug on.
 
62
Correctness if0 { `0 <= i` } (if !i>0 then i:=!i-1 else tt) { `0 <= i` }.
 
63
Omega.
 
64
Save.
 
65
 
 
66
(**********************************************************************)
 
67
 
 
68
Global Variable i : Z ref.
 
69
Debug on.
 
70
Correctness assert0 { `0 <= i` } begin assert { `i=2` }; i:=!i-1 end { `i=1` }.
 
71
 
 
72
(**********************************************************************)
 
73
 
 
74
Correctness echange
 
75
  { `0 <= i < N` /\ `0 <= j < N` }
 
76
  begin
 
77
    label B;
 
78
    x := t[!i]; t[!i] := t[!j]; t[!j] := !x;
 
79
    assert { #t[i] = #t@B[j] /\ #t[j] = #t@B[i] }
 
80
  end.
 
81
Proof.
 
82
Auto with datatypes.
 
83
Save.
 
84
 
 
85
  
 
86
(**********************************************************************)
 
87
 
 
88
(*
 
89
 *   while x <= y do x := x+1 done { y < x }
 
90
 *)
 
91
 
 
92
Correctness incrementation
 
93
  while !x < !y do
 
94
    { invariant True variant `(Zs y)-x` }
 
95
    x := !x + 1
 
96
  done
 
97
  { `y < x` }.
 
98
Proof.
 
99
Exact (Zwf_well_founded `0`).
 
100
Unfold Zwf. Omega.
 
101
Exact I.
 
102
Save.
 
103
 
 
104
 
 
105
(************************************************************************)
 
106
 
 
107
Correctness pivot1
 
108
  begin
 
109
    while (Z_lt_ge_dec !i r) do
 
110
      { invariant True variant (Zminus (Zs r) i) } i := (Zs !i)
 
111
    done;
 
112
    while (Z_lt_ge_dec r !j) do
 
113
      { invariant True variant (Zminus (Zs j) r) } j := (Zpred !j)
 
114
    done
 
115
  end
 
116
  { `j <= r` /\ `r <= i` }.
 
117
Proof.
 
118
Exact (Zwf_well_founded `0`).
 
119
Unfold Zwf. Omega.
 
120
Exact I.
 
121
Exact (Zwf_well_founded `0`).
 
122
Unfold Zwf. Unfold Zpred. Omega.
 
123
Exact I.
 
124
Omega.
 
125
Save.
 
126
 
 
127
 
 
128