*To*: Holger Gast <gast at informatik.uni-tuebingen.de>, 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:01:46 -0400*In-reply-to*: <535DFA1D.1050505@informatik.uni-tuebingen.de>*References*: <1398354631.4388.109993413.180C1388@webmail.messagingengine.com> <535DFA1D.1050505@informatik.uni-tuebingen.de>

Thank you Holger. I will certainly have look at your extensions. Cheers, George 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 [1]. > 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: > https://www21.in.tum.de/teaching/isv/SS13 > 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, > > Holger > > [1] Gast, H. "Semi-automatic proofs about object graphs in separation > logic", > in: Merz, S. and Lüttgen, G.: Automated Verification of Critical > Systems > (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. > > >

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

**Re: [isabelle] Simpl References Reasoning***From:*Holger Gast

- Previous by Date: Re: [isabelle] Simpl References Reasoning
- Next by Date: Re: [isabelle] Symbol Shortcuts vs. LaTeX code
- Previous by Thread: Re: [isabelle] Simpl References Reasoning
- Next by Thread: [isabelle] Hilbert's Basis Theorem
- 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