Ilya Sergey
Ilya Sergey
Implement a predicate for skip-list and basic operations on it. A good example is given in this paper: https://www.irif.fr/~sighirea/spen/FIT-TR-2014-01.pdf
Depends on issue #10 and takes the similar example into the account. This should beneficial for all examples implementing traversals and manipulations.
When running `suslik -r true`, a trace is shown. The successful subderivations of the synthesiser correspond to the trees. It would be good to have this tree captured as a...
At the moment, synthesis can take "hints" about auxiliary functions, which can be used for synthesing the main one. For instance, this is a specification for tree flattening that takes...
As an example, consider the `list_copy` specification: ``` { r :-> x ** lseg(x, S) } void listcopy(loc r) { r :-> y ** lseg(x, S) ** lseg(y, S) }...
Implement a specification for de-allocating/copying a list of lists of integers. Synthesize it if given a hint about a specification of the corresponding auxiliary function that for simple lists of...
* Checking that no funds go unaccounted * Uses a dedicated type for Money
Currently pure terms (`Syntax.expr`) bears only location infor for identifiers, but not for expressions, which makes it difficult to report type errors.
The following snipped is not indented correctly: ``` match A with | _ -> expr = {something ; something_else} ```