*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Simpl References Reasoning*From*: Thomas Sewell <thomas.sewell at nicta.com.au>*Date*: Mon, 28 Apr 2014 11:31:46 +1000*In-reply-to*: <1398354631.4388.109993413.180C1388@webmail.messagingengine.com>*References*: <1398354631.4388.109993413.180C1388@webmail.messagingengine.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.4.0

Hello George.

I can fix your proof by extending First_spec as follows: lemma (in First_impl) First_spec: " \<forall>\<sigma> x. \<Gamma>,\<Theta> \<turnstile>\<^sub>t

\<acute>result' :== PROC First(\<acute>x)

\<and> \<acute>free = \<^bsup>\<sigma>\<^esup>free - sz_First

" (you might have to save that and load it in jEdit to read it).

Good luck, Thomas. On 25/04/14 01:50, George K. wrote:

Hello all, I have been using Schirmer's Simpl for the past couple of months now. I am stuck when trying to reason with a procedure that deals with references. In particular, I cannot discharge the procedure's specification when the procedure calls other procedures that allocate memory and set field values. I am attaching a theory that illustrates the issues I have. This theory contains: 1) A globals_memory hoarestate, containing a list of allocated references and a free counter of available memory. Taken straight out of the examples of the AFP SIMPL distro. 2) A globals_First hoarestate that declares a data structure that just holds a single field of int type 3) A procedure First() that is, in essence, a constructor. 4) A globals_Second hoarestate which contain two fields each one being a "ref => ref". The intent is to model a data structure that contains references to other structures. 5) A Second_1 procedure that is a constructor accepting a two references. 6) A Second_2 procedure that is also a constructor--however, we pass integer values and invoke the First() procedure twice. It is this procedure I cannot prove the functional specification. The functional spec looks as follows: lemma (in Second_2_impl) Second_2_spec: " ∀σ x1 x2. Γ,Θ ⊢⇩t ⦃σ. ´x1 = x1 ∧ ´x2 = x2 ∧ (sz_Second + sz_First + sz_First) ≤ ´free ⦄ ´result' :== PROC Second_2(´x1,´x2) ⦃ ´result' ≠ Null ∧ ´result'→´Y ≠ Null ∧ ´result'→´Z ≠ Null ∧ ´free = ⇗σ⇖free - sz_Second - sz_First - sz_First ∧ ´result'→´Z→´X = x2 ∧ ´result'→´Y→´X = x1 ∧ ´result' ∈ set ´alloc ⦄ " The last two conjucts (i.e. ´result'→´Y→´X = x1 ∧ ´result' ∈ set ´alloc) are giving me hard time. I believe the issues I have are related to letting Isabelle know that the references allocated within the Second_2 procedure are distinct (at least this is what I understand when reading on the split heap model used in Simpl). Unfortunately, I am not sure how I can express this kind of distinctness in Isabelle. Furthermore, I am unsure on whether I need to abstract simple data structures (such as the one in the attached theory) in HOL, similarly to the manner linked lists in the heap are abstracted to HOL lists using the List predicate. Any help is appreciated. George.

**Follow-Ups**:**Re: [isabelle] Simpl References Reasoning***From:*George K.

**References**:**[isabelle] Simpl References Reasoning***From:*George K.

- Previous by Date: [isabelle] Isar polymorphism problem
- Next by Date: Re: [isabelle] Simpl References Reasoning
- Previous by Thread: [isabelle] Simpl References Reasoning
- Next by Thread: Re: [isabelle] Simpl References Reasoning
- Cl-isabelle-users April 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list