← Back to branch summary

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

« back to all changes in this revision

Viewing changes to contrib/correctness/Arrays.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/Arrays.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(* Certification of Imperative Programs / Jean-Christophe Filli�tre *)
 
10
 
 
11
(* $Id: Arrays.v 5920 2004-07-16 20:01:26Z herbelin $ *)
 
12
 
 
13
(**********************************************)
 
14
(* Functional arrays, for use in Correctness. *)
 
15
(**********************************************)
 
16
 
 
17
(* This is an axiomatization of arrays.
 
18
 *
 
19
 * The type (array N T) is the type of arrays ranging from 0 to N-1 
 
20
 * which elements are of type T.
 
21
 *
 
22
 * Arrays are created with new, accessed with access and modified with store. 
 
23
 *
 
24
 * Operations of accessing and storing are not guarded, but axioms are.
 
25
 * So these arrays can be viewed as arrays where accessing and storing
 
26
 * out of the bounds has no effect.
 
27
 *)
 
28
 
 
29
 
 
30
Require Export ProgInt.
 
31
 
 
32
Set Implicit Arguments.
 
33
 
 
34
 
 
35
(* The type of arrays *)
 
36
 
 
37
Parameter array : Z -> Set -> Set.
 
38
 
 
39
 
 
40
(* Functions to create, access and modify arrays *)
 
41
 
 
42
Parameter new : forall (n:Z) (T:Set), T -> array n T.
 
43
 
 
44
Parameter access : forall (n:Z) (T:Set), array n T -> Z -> T.
 
45
 
 
46
Parameter store : forall (n:Z) (T:Set), array n T -> Z -> T -> array n T.
 
47
 
 
48
 
 
49
(* Axioms *)
 
50
 
 
51
Axiom
 
52
  new_def :
 
53
    forall (n:Z) (T:Set) (v0:T) (i:Z),
 
54
      (0 <= i < n)%Z -> access (new n v0) i = v0.
 
55
 
 
56
Axiom
 
57
  store_def_1 :
 
58
    forall (n:Z) (T:Set) (t:array n T) (v:T) (i:Z),
 
59
      (0 <= i < n)%Z -> access (store t i v) i = v.
 
60
 
 
61
Axiom
 
62
  store_def_2 :
 
63
    forall (n:Z) (T:Set) (t:array n T) (v:T) (i j:Z),
 
64
      (0 <= i < n)%Z ->
 
65
      (0 <= j < n)%Z -> i <> j -> access (store t i v) j = access t j.
 
66
 
 
67
Hint Resolve new_def store_def_1 store_def_2: datatypes v62.
 
68
 
 
69
(* A tactic to simplify access in arrays *)
 
70
 
 
71
Ltac array_access i j H :=
 
72
  elim (Z_eq_dec i j);
 
73
   [ intro H; rewrite H; rewrite store_def_1
 
74
   | intro H; rewrite store_def_2; [ idtac | idtac | idtac | exact H ] ].
 
75
 
 
76
(* Symbolic notation for access *)
 
77
 
 
78
Notation "# t [ c ]" := (access t c) (at level 0, t at level 0).
 
 
b'\\ No newline at end of file'