Re: [isabelle] Annotations in Simpl



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?

  -- Lars





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