Re: [isabelle] Annotations in Simpl



On 10/07/2012, at 9:21 PM, Lars Noschinski wrote:

> On 10.07.2012 11:27, Gerwin Klein wrote:
>> On the other hand, depending on the use context you might just be interested in the fact that a certain function doesn't change certain parts of the state. This can be a completely automatic proof where you don't even have to state the specification, because a tool can figure it out for you. But if you are only allowed to have precisely one specification per function, you can't make use of such simple automatic side proofs.
> 
> I guess, Simpl accounts for this case with the _modifies specifications?

Yes, Simpl does, and a few other frameworks have the same special case, because it occurs so often that it can't be ignored. There is nothing in between, though. If your memory model has separate heap framing conditions, you're already out of luck.

Simpl can easily be extended to allow the vcg to use an arbitrary lemma as spec for a function to get all that (not sure if we've pushed that change to the AFP yet -- we should). With that, there is only the problem of nice syntax for annotations left.

Cheers,
Gerwin






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