*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Simpl References Reasoning*From*: "George K." <g_karab at encs.concordia.ca>*Date*: Mon, 28 Apr 2014 12:00:31 -0400*In-reply-to*: <535DAF82.2080201@nicta.com.au>*References*: <1398354631.4388.109993413.180C1388@webmail.messagingengine.com> <535DAF82.2080201@nicta.com.au>

Thank you Thomas! Indeed this is tedious, but it does make sense. My initial understanding was that specifying the frame condition would suffice but I was wrong. I will start tackling Separation Logic as soon as I can. Cheers, George On Sun, Apr 27, 2014, at 09:31 PM, Thomas Sewell wrote: > Hello George. > > Indeed you need a lot of distinctness. The problem with this kind of > hoare level reasoning about heaps is that you need to establish not only > that the modified values are modified as expected, but that everything > else is unchanged. > > 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 > \<lbrace>\<sigma>. \<acute>x = x \<and> sz_First \<le> > \<acute>free \<rbrace> > \<acute>result' :== PROC First(\<acute>x) > \<lbrace> \<acute>result' \<noteq> Null \<and> > \<acute>result'\<rightarrow>\<acute>X = x \<and> > \<acute>result' \<in> set \<acute>alloc \<and> > \<acute>result' \<notin> set (\<^bsup>\<sigma>\<^esup>alloc) > \<and> set \<acute>alloc = insert \<acute>result' (set > (\<^bsup>\<sigma>\<^esup>alloc)) > \<and> \<acute>free = \<^bsup>\<sigma>\<^esup>free - sz_First > \<and> (\<forall>x \<in> set > (\<^bsup>\<sigma>\<^esup>alloc). x\<rightarrow>\<acute>X = > x\<rightarrow>\<^bsup>\<sigma>\<^esup>X )\<rbrace> > " > > (you might have to save that and load it in jEdit to read it). > > I've additionally asserted that the allocated address was not previously > allocated, that the set of allocated addresses has grown by the one > allocated address, and that all values previously allocated are > unchanged. > > The current fashion is to avoid this tedious enumeration of everything > that stays the same by using some kind of separation logic. Perhaps you > should investigate whether Simpl provides something like that, or some > standard idiom for expressing what hasn't changed. > > 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. > >

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

**Re: [isabelle] Simpl References Reasoning***From:*Thomas Sewell

- Previous by Date: Re: [isabelle] Isar polymorphism problem
- Next by Date: Re: [isabelle] Simpl References Reasoning
- Previous by Thread: Re: [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