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.

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.
> 
>




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.