Re: [isabelle] Simpl References Reasoning
Thank you Holger. I will certainly have look at your extensions.
On Mon, Apr 28, 2014, at 02:50 AM, Holger Gast wrote:
> Hello George,
> Thomas mentions using separation logic in his reply.
> As it happens, I have build the usual symbolic
> execution approach on top of Simpl for a project .
> The basic idea is to reconstruct the original execution
> sequence of heap operations as much as necessary in the form
> of nested let expressions, by considering the nesting
> of the heap access expressions and various side-conditions.
> The latest version of the implementation is available from
> the homepage of last year's lecture on software verification:
> The file SimplC.zip also contains a (rudimentary)
> C parser, translator to Simpl, the reconstruction
> mentioned above, and symbolic execution/heap matching.
> Hope this helps,
>  Gast, H. "Semi-automatic proofs about object graphs in separation
> in: Merz, S. and Lüttgen, G.: Automated Verification of Critical
> (AVoCS '12)
> On 04/24/2014 05:50 PM, 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