Re: [isabelle] Simpl References Reasoning
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.
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
> \<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
> 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,
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and