(* * Seplog is an implementation of separation logic (an extension of Hoare * logic by John C. Reynolds, Peter W. O'Hearn, and colleagues) in the * Coq proof assistant (version 8, http://coq.inria.fr) together with a * sample verification of the heap manager of the Topsy operating system * (version 2, http://www.topsy.net). More information is available at * http://web.yl.is.s.u-tokyo.ac.jp/~affeldt/seplog. * * Copyright (c) 2005, 2006 Reynald Affeldt and Nicolas Marti * * This program is free software; you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by * the Free Software Foundation; either version 2 of the License, or * (at your option) any later version. * * This program is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with this program; if not, write to the Free Software * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA *) Load seplog_header. Require Import frag. (* A simple one: swap *) Definition i : var.v := 1. Definition j : var.v := 2. Definition x : var.v := 4. Definition y : var.v := 3. Definition swap (x y:var.v) : cmd := i <-* var_e x; j <-* var_e y; var_e x *<- var_e j; var_e y *<- var_e i. Definition swap_precond (x y:var.v) (vx vy : Z) : assrt := (true_b, star (singl (var_e x) (int_e vx)) (singl (var_e y) (int_e vy))). Definition swap_postcond (x y:var.v) (vx vy : Z) : assrt := (true_b, star (singl (var_e x) (int_e vy)) (singl (var_e y) (int_e vx))). Lemma swap_verif: forall vx vy, {{assrt_interp (swap_precond x y vx vy)}} swap x y {{assrt_interp (swap_postcond x y vx vy)}}. intros. unfold swap_precond. unfold swap_postcond. eapply LWP_use. simpl; intuition. unfold x; unfold y; unfold i; unfold j. (* step-by-step proof *) (*LWP_turnl. apply LWP_lookup. Omega_exprb. LWP_turnl. eapply LWP_subst_lookup'. Omega_exprb. simpl; intuition. apply LWP_subst_mutation. simpl. LWP_turnl. apply LWP_mutation. Omega_exprb. apply LWP_subst_mutation. simpl. LWP_turnl. apply LWP_mutation. Omega_exprb. apply LWP_subst_elt. simpl. apply LWP_star_elim. Omega_exprb. Omega_exprb. apply LWP_epsintror. apply LWP_comr. apply LWP_epsintrol. apply LWP_coml. apply LWP_star_elim. Omega_exprb. Omega_exprb. apply LWP_tauto. Omega_exprb.*) LWP_Resolve. Qed. (* an initialization of a field for an array of structure *) Definition ptr : var.v :=1. Definition startl : var.v := 2. Fixpoint init_body (n size idx: nat) (init_val: Z) {struct n}: cmd := match n with 0 => skip | S n' => (ptr -.> Z_of_nat idx) *<- int_e init_val; ptr <- (var_e ptr) +e (nat_e size); init_body n' size idx init_val end. Definition init (n: nat) (startl :var.v) (size idx: nat) (init_val: Z): cmd := ptr <- var_e startl; init_body n size idx init_val. Fixpoint init_precond_sigma (n: nat) (startl :var.v) (size idx: nat) (init_val: Z) {struct n} : Sigma := match n with 0 => epsi | S n' => star (cell ((startl -.> Z_of_nat idx) +e (nat_e (size*n')))) (init_precond_sigma n' startl size idx init_val) end. Definition init_precond (n: nat) (startl :var.v) (size idx : nat) (init_val: Z) : assrt := (var_e startl >> int_e 0%Z, init_precond_sigma n startl size idx init_val). Fixpoint init_postcond_sigma (n: nat) (startl :var.v) (size idx: nat) (init_val: Z) {struct n}: Sigma := match n with 0 => epsi | S n' => star (singl ((startl -.> Z_of_nat idx) +e (nat_e (n'*size))) (int_e init_val)) (init_postcond_sigma n' startl size idx init_val) end. Definition init_postcond (n: nat) (startl :var.v) (size idx: nat) (init_val: Z) : assrt := (var_e startl >> int_e 0%Z, init_postcond_sigma n startl size idx init_val). Open Local Scope dec_frag_scope. Lemma init_verif: forall n size field_indice init_val, n = 6 -> [[init_precond n startl size field_indice init_val]] (init n startl size field_indice init_val) [[init_postcond n startl size field_indice init_val]]. intros; subst n. unfold init; simpl init_body. unfold init_precond; simpl init_precond_sigma. unfold init_postcond; simpl init_postcond_sigma. unfold field; unfold ptr; unfold startl. eapply LWP_use. simpl; intuition. (* step-by-step proof for n=2 *) (*apply LWP_subst_mutation. simpl. LWP_turnl. LWP_turnl. LWP_turnl. apply LWP_mutation'. Omega_exprb. apply LWP_subst_subst. simpl. apply LWP_subst_mutation. simpl. LWP_turnl. apply LWP_mutation'. Omega_exprb. apply LWP_subst_subst. simpl. apply LWP_subst_elt. simpl. LWP_turnr. LWP_turnr. apply LWP_epselimr. LWP_turnl. apply LWP_epseliml. apply LWP_star_elim. Omega_exprb. Omega_exprb. apply LWP_epsintror. LWP_turnr. apply LWP_epsintrol. LWP_turnl. apply LWP_star_elim. Omega_exprb. Omega_exprb. apply LWP_tauto. Omega_exprb.*) LWP_Resolve. Qed. (* Lemma init_verif': forall n size field_indice init_val, [[init_precond n startl size field_indice init_val]] (init n startl size field_indice init_val) [[init_postcond n startl size field_indice init_val]]. induction n. unfold init; simpl init_body. unfold init_precond; simpl init_precond_sigma. unfold init_postcond; simpl init_postcond_sigma. unfold field; unfold ptr; unfold startl. intros. eapply LWP_use. simpl; intuition. LWP_Resolve. unfold init; simpl init_body. unfold init_precond; simpl init_precond_sigma. unfold init_postcond; simpl init_postcond_sigma. unfold field; unfold ptr; unfold startl. intros. *) Require Import ZArith. Open Local Scope Z_scope. (* Inductive array: expr -> expr -> store.s -> heap.h -> Prop := array_emp: forall e1 e2 s h, sep.emp s h -> eval e1 s = eval (nat_e 0) s -> eval e2 s = eval (nat_e 0) s -> array e1 e2 s h | array_suiv: forall e1 e2 s h h1 h2, h1 # h2 -> h = (h1 +++ h2) -> eval (e2) s > eval (nat_e 0) s -> (exists v, (e1 |-> (int_e v)) s h1) -> array (e1 +e (nat_e 1)) (e2 -e (nat_e 1)) s h2 -> array e1 e2 s h. Axiom array_concat_split_left: forall size size' adr s h, array adr size s h -> eval size' s >= eval (nat_e 0) s -> eval size s <= eval size' s -> (array adr size' ** array (adr +e size') (size -e size')) s h. *)