search

kiniry / Mobius

4 stars 8 forks source link

double-check refinement checking from queries to fields #713

Open atiti opened 11 years ago

atiti commented 11 years ago

A student in my AMP class reported this is not reliable.

atiti commented 11 years ago

From: kiniry (GH: kiniry) Date: Thu Mar 31 09:56:10 2011

In particular, if a query has a postcondition and it is refined to a field, then the field's invariant should be that postcondition.