AutoCorres abstraction allows me to prove an invalid Hoare triple about l4v

[lsf37]

Hi Scott,

in the test file you're using the partial correctness Hoare triples that assume guards and asserts (which pointer validity is translated to).

To get the ones you want, you'd either prove "no_fail P f" independently, or you'd use the total correctness triples (validNF, i.e. the "<lbrace> .. <rbrace> f <lambda> .. <rbrace>!" syntax -- note the "!" at the end).

Cheers,
Gerwin

[lsf37]

Just to explain why this strange division (we recently had a discussion about this internally as well): in our refinement proofs, no_fail is implied by the refinement we're proving, so it'd be wasted effort to prove it twice -- that's why there is a version of Hoare triples that assume them instead of asserting them, and it's also the reason that version is the default syntax.

[talsewell]

Um, on that issue, there's another aspect. One useful but unusual feature of the "wp" proof approach is the way we've approached specialisation. So, if you need to prove {P} f {Q and R}, you can build this out of proofs {P1} f {Q}, {P2} f {R}, etc. These smaller proof fragments might seem overspecialised, but once you get down to the building blocks of your invariants, the fragments may actually be quite reusable. Anyway, for that approach to work, it has to be partial validity. Otherwise every one of these proof fragments would need to establish the same correctness properties. Cheers, Thomas. On 22/03/17 10:30, Gerwin Klein wrote: Just to explain why this strange division (we recently had a discussion about this internally as well): in our refinement proofs, no_fail is implied by the refinement we're proving, so it'd be wasted effort to prove it twice -- that's why there is a version of Hoare triples that assume them instead of asserting them, and it's also the reason that version is the default syntax. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub<#18 (comment)>, or mute the thread<https://github.com/notifications/unsubscribe-auth/ANQQ8BQK7t_A7nGQnDxnScsQNULdajxxks5roF2hgaJpZM4MkJB1>.

[sdconsta]

Excellent explanations from both of you. This fully explains the behavior I was witnessing. Thanks!

Scott