#
ae90f552 |
|
05-Jan-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
This is a major refactoring of the separation-logic example. The main changes are: - the smallfoot case study has been renamed to "holfoot" - a lot of the results of the smallfoot case study were generalised to the "variables as resource" level of abstraction - this generalisation allows much shorter and easier proofs for the remaining results - new methods for handling conditional execution, while-loops and procedure calls implemented - generalisation of the concept of ghost variables (e.g. limitation on the possible types of ghost variables removed) - addition of comments that keep track of the current position in the program, thereby giving useful feedback to the user during interactive proofs or when a proof-attempt fails - rewritten automation in order to - make extensions of the programming and specification language easier - keep track of location comments - increase speed - pretty printing uses styles (i.e. colors, bold fonts, etc.) now - tree predicate of smallfoot generalised to allow data in trees as well as arbitrary n-ary trees - holfoot command line tool added
|