Re: [isabelle] Simpl References Reasoning

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:
The file also contains a (rudimentary)
C parser, translator to Simpl, the reconstruction
mentioned above, and symbolic execution/heap matching.

Hope this helps,


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

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