#
4e1408fc |
|
15-Aug-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove trailing whitespace throughout examples/
|
#
a45f24f5 |
|
28-Nov-2016 |
Thomas Tuerk <thomas@tuerk-brechen.de> |
holfoot example: add selftests
|
#
e6bbfa31 |
|
23-Nov-2015 |
Thomas Tuerk <Thomas.Tuerk@fireeye.com> |
Holfoot example: remove some bit rot some of Holfoot's examples might be broken, not checked yet
|
#
bd77b8fb |
|
20-Oct-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Delete trailing whitespace
|
#
e8736117 |
|
27-Dec-2012 |
Thomas Tuerk <tt291@cl.cam.ac.uk> |
minor tweaks on quantHeuristicsLib, adept Holfoot to changes with MEM
|
#
0ab70425 |
|
11-Oct-2012 |
Thomas Tuerk <tt291@cl.cam.ac.uk> |
holfoot: REPLACE_ELEMENT -> LUPDATE - adapt to recent renaming of REPLACE_ELEMENT to LUPDATE - cleaning up generalHelpersScript
|
#
4480c57d |
|
24-Aug-2012 |
Thomas Tuerk <tt291@cl.cam.ac.uk> |
cleanup of quantifier heuristics library - more sensible names for guesses - quantHeuristicsLib renamed to quantHeuristicsLibBase - quantHeuristicsLibArgs renamed to quantHeuristicsLibParameters - new shorter signature defined in quantHeuristicsLib - adaptation of usage of quantHeuristicsLib
|
#
845531b5 |
|
14-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove trailing whitespace in source files.
|
#
cb1d9f1e |
|
18-Sep-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
adaptation to changes in quantHeuristicsLib and permLib, rotate example added
|
#
2469f641 |
|
06-Sep-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
support for global specification variables added to the parser
|
#
7ae505c4 |
|
27-Aug-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
Examples from VSTTE-competition added. For example vscomp4 the parser was modified to support user defined predicates. As part of this change the syntax for trees changed.
|
#
b4041775 |
|
02-Aug-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
- equal splitting of permissions removed from vars_as_resourceScript - fixed building Holfoot binaries for MacOS - minor cleanups in separationLogicScript - move MP_CANON to Drule - minor extendion to the automation of frame calculations with points-to predicates - example list_alloc_dealloc_length.dsf from THOR paper added
|
#
a12ff234 |
|
28-Jun-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
- fix a bug in the printout of the automated procedures that prevented using being used on input files that contain assumed procedure specifications - some more cleanup of separationLogicScript - tiny generalisation of lists in holfoot which might in the far future be used for double linked lists
|
#
b9ee1596 |
|
23-Jun-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
rename most occurences of the prefix "FASL" into "ASL" The prefix ASL (Abstract Separation Logic) was used to indicate definitions related to Abstract Separation Logic. To distinguish definitions that were not aware of the special failiure state (like asl_star) and ones that were (fasl_star) the additional prefix FASL (Abstract Separation Logic with Failiure State) was used as well. However, in the end, most definitions had the FASL prefix which does not make much sense. So, the prefix was replaced by ASL expect for cases where it is really important to distinguish between versions of a definition that are aware of the failiure state and ones that are not.
|
#
c2243bd8 |
|
06-Jun-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
strengthening of splitting intervals, new example of reversing an array added
|
#
0c2b3a1f |
|
28-May-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
fix problems with mosml-version
|
#
36ac5139 |
|
26-May-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
extensions of the interface / easier addition of own tactics
|
#
f8c63b1c |
|
20-May-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
- add multiple levels for expansions by holfoot-tactics, there were no_expands and do_expands, now there is full_expands as well. full_expands behaves like the old do_expands. do_expands does just fast expansions now - fix a bug in the handling of assertions - example array-inc added - example quicksort-full-loopspec added
|
#
498c8ca3 |
|
13-May-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
Update of the interactive proof-scripts to make them better usable for the web-interface. Now some unimportant output is discarded and (more importantly) examples that are intended to fail are put into commented out.
|
#
00d70507 |
|
06-May-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
Added an option to the command-line tool to run interactive proof scripts. The proof scripts have been updated to work with this new feature.
|
#
44fc624c |
|
26-Mar-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
some optimisations on how to use Yices
|
#
d96b2822 |
|
25-Mar-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
added a binary-search example that shows the usefulness of Yices
|
#
e6f852f0 |
|
24-Mar-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
some more work on arrays, especially modifying predicate simpsets
|
#
d32bdb3a |
|
20-Mar-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
some optimisations for arrays / support for HolSmtLib added
|
#
701ed3b9 |
|
20-Mar-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
some more support for arrays and a new q uicksort example using arrays
|
#
89dae6d7 |
|
18-Mar-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
- adaption to the recent changes to listTheory / listSimps / rich_listTheory. - some support for arrays added
|
#
60371203 |
|
05-Mar-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
Mayor refactoring of the Holfoot-Parser. The parser now uses the abstract syntax of HOL internally, which allows it to pass typing information between different parts of the input much more efficiently. As a result, most type-annotations could be removed from the input files. Moreover, it's now possible to write HOL terms as expressions inside a program now. These expressions have to return a value of type num and may take program variables as input. For example programs like "x = ``MAX y z``" can be written now, where "x", "y" and "z" are variables of the programming language. A similar extension has been added for conditions of loops and if-then-else statements. Finally, there is a predicate for separating mapping and predicate for queues now.
|
#
21cb3f4e |
|
15-Feb-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
- make holfoot work again after the changes to the simplifier (arithmetic decision procedure) - a lot of cleaning up of problems found by sanity-checks - introduction of var_res_bigstar as a first step towards adding arrays
|
#
8df49b38 |
|
05-Feb-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
getting holfoot working with mosml
|
#
775fada5 |
|
04-Feb-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
A lot of minor changes, mainly in the behaviour of the web-interface and the command-line tool. Step-wise tool for the web added.
|
#
64490314 |
|
25-Jan-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
some minor improvements on the command line tool and the holfoot
|
#
444f3457 |
|
24-Jan-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
A lot of minor changes: - introduction of gen_step_tac_opt, i.e. new interface to most holfoot tactics - stopping simulation at specific points like loops, abstractions etc. added - renaming of holfoot tactics - better support for LAST and FIRST in specifications - holfoot_interactive_verify_spec and similar functions improved - holfoot_set_goal_preprocess and holfoot_set_goal_procedures added
|
#
efdf9745 |
|
20-Jan-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
improvements to the parser (better error reporting, more arithmetic operations) as well as addition of loop- and block-specifications with corresponding examples
|
#
20606eca |
|
15-Jan-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
easier building of holfoot, extensions to the command line tool to support html-output
|
#
fdc84b40 |
|
14-Jan-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
A lot of minor tweaks and additions. The main ones are: - parser can handle trees better now - better support for call-by-value arguments by the parser - inference for splitting of non-empty trees added - option to turn of expanding specifications added to main tactics - NUM_TO_BOOL added - slightly extended treeTheory
|
#
0076aa8e |
|
08-Jan-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
some minor fixes and extensions: - parser allows call-by-value arguments in HOL-expressions now - fixing pretty printing problem of call-by-reference arguments in abstracted function calls - some minor changes in the order of inference applications
|
#
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
|