Alice_rs is a small proof-of-concept reference implementation of a decision procedure for A Decidable Fragment of Separation Logic and was written as supplemental material for this seminar paper. The name comes from a wrong pronunciation of the ls structure. The correct pronunciation would be "list structure" but it could also be read as "al-as structure" which sounds a bit like alice.
Alice_rs is currently only available through this repository.
It is recommended to use a current version of the rust language compiler with cargo. Both can be obtained from here.
The build process is based around the standard cargo build tool chain (it is recommended for non development builds to use the --release flag):
cargo buildAlice_rs takes an entailment as a string command line argument like this: alice_rs "[here goes the entailment]".
Example:
alice_rs "And[Neq(x,y)]|SepConj[x->y,y->Nil] |- True|SepConj[ls(x, Nil)]"For those unexperienced in this kind of separation logic, here is a short introduction to the semantics:
An entailment describes that for all states (a formal description of a stack and heap architecture) for which the left formula holds the right formula should hold as well.
A formula consists of statements about a state.
These statements are organized in two parts: first the pure logic (reasons about equality) and the spatial logic (reasons about the heap structure).
For more information please have a look at the theoretical background mentioned above (this and this).
The grammar for the entailment strings is based on standard separation logic formulæ (definitions in order of priority):
| Nonterminal | Definition | |
|---|---|---|
| Entailment | → | Formula |- Formula |
| Formula | → | Pure | Spatial |
| Pure | → | True |
| Pure | → | And[Op_Vec] |
| Op_Vec | → | Op, Op_Vec |
| Op_Vec | → | Op |
| Op | → | Eq(Expr, Expr) |
| Op | → | Neq(Expr, Expr) |
| Spatial | → | Emp |
| Spatial | → | SepConj[Spatial_Vec] |
| Spatial_Vec | → | AtomicSpatial, Spatial_Vec |
| Spatial_Vec | → | AtomicSpatial |
| AtomicSpatial | → | Expr -> Expr |
| AtomicSpatial | → | ls(Expr, Expr) |
| Expr | → | Nil |
| Expr | → | [a-zA-z]+ |
To run in the development environment simply use cargo run [here goes the entailment] (the --release flag can be used with this as well.
Tests can be run with cargo test.
If the program returns nothing, the entailment is valid. Otherwise either a parser error occurred or the entailment is found invalid. These errors are currently only handled via rust's panic mechanism. A more sophisticated error handling is yet to be implemented.
Despite this project being a complete proof-of-concept implementation further development is planned. Especially the internal representation will be the issue of further improvements.
See the Contributing file.
Alice_rs is licensed under the MIT license.