diff options
author | 2003-11-29 16:15:58 +0000 | |
---|---|---|
committer | 2003-11-29 16:15:58 +0000 | |
commit | 9058fb97426307536f56c3e7447be2f70798e081 (patch) | |
tree | b9a5fcf2ace7ecec13ed264b93c33fc04b0f220f /contrib7/correctness/Arrays.v | |
parent | 95ad10e5eb2efc9b63382e0e6a2f9ada8da2ea2d (diff) |
Deplacement des fichiers ancienne syntaxe dans theories7, contrib7 et states7
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5026 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib7/correctness/Arrays.v')
-rw-r--r-- | contrib7/correctness/Arrays.v | 75 |
1 files changed, 75 insertions, 0 deletions
diff --git a/contrib7/correctness/Arrays.v b/contrib7/correctness/Arrays.v new file mode 100644 index 000000000..40b19e74f --- /dev/null +++ b/contrib7/correctness/Arrays.v @@ -0,0 +1,75 @@ +(***********************************************************************) +(* 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$ *) + +(**********************************************) +(* Functional arrays, for use in Correctness. *) +(**********************************************) + +(* This is an axiomatization of arrays. + * + * The type (array N T) is the type of arrays ranging from 0 to N-1 + * which elements are of type T. + * + * Arrays are created with new, accessed with access and modified with store. + * + * Operations of accessing and storing are not guarded, but axioms are. + * So these arrays can be viewed as arrays where accessing and storing + * out of the bounds has no effect. + *) + + +Require Export ProgInt. + +Set Implicit Arguments. + + +(* The type of arrays *) + +Parameter array : Z -> Set -> Set. + + +(* Functions to create, access and modify arrays *) + +Parameter new : (n:Z)(T:Set) T -> (array n T). + +Parameter access : (n:Z)(T:Set) (array n T) -> Z -> T. + +Parameter store : (n:Z)(T:Set) (array n T) -> Z -> T -> (array n T). + + +(* Axioms *) + +Axiom new_def : (n:Z)(T:Set)(v0:T) + (i:Z) `0<=i<n` -> (access (new n v0) i) = v0. + +Axiom store_def_1 : (n:Z)(T:Set)(t:(array n T))(v:T) + (i:Z) `0<=i<n` -> + (access (store t i v) i) = v. + +Axiom store_def_2 : (n:Z)(T:Set)(t:(array n T))(v:T) + (i:Z)(j:Z) `0<=i<n` -> `0<=j<n` -> + `i <> j` -> + (access (store t i v) j) = (access t j). + +Hints Resolve new_def store_def_1 store_def_2 : datatypes v62. + +(* A tactic to simplify access in arrays *) + +Tactic Definition ArrayAccess i j H := + Elim (Z_eq_dec i j); [ + Intro H; Rewrite H; Rewrite store_def_1 + | Intro H; Rewrite store_def_2; [ Idtac | Idtac | Idtac | Exact H ] ]. + +(* Symbolic notation for access *) + +Notation "# t [ c ]" := (access t c) (at level 0, t ident) + V8only (at level 0, t at level 0). |