OS X / Linux:
Windows:
- Get Haskell Platform
- Get Z3
- Get the Literate Unit-B source
- Compiling the utilities package
- Compiling the Unit-B program
- Run the test suite
Download the Haskell platform at https://www.haskell.org/
Z3 can be obtained from http://z3.codeplex.com/ and should be placed in the PATH. Be sure to get version 4.3.2, hashcode 2ca14b49fe45.
As a rule, do not publish a commit unless (0) the tests have been run just before the commit and (1) the tests are successful.
In order to stay up to date with the project's lead developments (today known under the pseudonym cipher1024), enter the command:
> git remote cipher https://[email protected]/cipher2048/literate-unitb.git
then, any time you need to update one of the branches (most likely the master branch):
> git pull cipher master
In order to compile Literate Unit-B, you need a number of Haskell libraries which you can install using cabal in the command line.
> cd utils
> cabal install
> cd ..
> cabal install
First, at the root of literate-unitb, create a directory called bin and put the binary executable of z3. Second, open a terminal at the root of literate-unitb and type
> cabal run run_tests
A series of test results should appear ending with
***********
* SUCCESS *
***********
First off, use the install-stylesheets-macosx.hs script in the
unitb/literate-unitb-scripts
repo to copy the required LaTeX style files to their destination.
On Linux, the destination path is ~/texmf/tex/.
In a terminal, launch
> unitb -c source-file.tex
This will lauch Literate Unit-B in continuous (or interactive) mode. As source-file.tex (or any file it inputs) gets updated, Literate Unit-B regenerates the proof obligations and tries any new one.
The command
> unitb source-file.tex
will launch one verification and terminate.
The suggested workflow is to integrate Literate Unit-B to a LaTeX creation workflow and to keep the terminal in sight to see failed verification.
Use the style-sheet unitb.sty provided in Tests/
\begin{machine}{} -- -- Structural declaration -- \refines{} \newset{} name can be a command \newevent{}{} we use to refer to the event when adding assignments and \with{} available theories: * sets * functions * arithmetic * predcalc * intervals -- -- Symbol declaration -- \variable{ sym1, .., symN : Type } declares sym1 to symN as variables of the enclosing machine \constant{ sym1, .., symN : Type } declares sym1 to symN as variables of the context of the machine \dummy{ sym1, .., symN : Type } declares sym1 to symN as dummies and gives them types in quantifiers when the context does not make the type of bound variables clear \indices{}{ sym1, .., symN : Type } \param{}{ sym1, .., symN : Type } declare sym1 to symN as indices (or parameters) of event -- -- New expressions -- # Context \assumption{}{} # Machine expressions \initialization{}{} \invariant{}{} \transient{}{}{} \transientB{}{}{}{} hints can contain: \index{}{} for example \index{pid}{head.queue} would choose an event whose index is at the head of a queue \witness{}{} \witness{pid}{pid' \in free} chooses any free process id to falsify the transient predicate \lt{} When \transientB names an event with a fine schedule, the progress property ensures that the fine schedule is true infinitely often if the transient predicate remains true continually. \constraint{}{} \safety{}{}{} \safety{lbl}{p}{q} declares the property p unless q \safetyB{}{}{}{} \safetyB{lbl}{evt}{p}{q} declares the property p unless q except evt \progress{}{}{} # Event expressions \evguard{}{}{} \cschedule{}{}{} \fschedule{}{}{} \evassignment{}{}{} \evbcmeq{}{}{}{} \evbcmsuch{}{}{}{} \evbcmin{}{}{}{} # Refinement and Proofs \refine{}{}{}{} \replace{}{}{}{}{}{} \replace{evt}{old}{new}{supp}{prog}{saf} removes old, replace them with new and uses supp in the proof. prog and saf have to establish: old ∧ supp |-> new ∧ supp new ∧ supp unless ¬(old ∧ supp) \weakento{}{}{} Deletes the old coarse schedules and replace them with the new weaker ones. When designing a new scheduled event, the "default" schedule, false, has to be weakened in order to apply fairness to the new event. \replacefine{}{}{}{} \removeguard{}{} \begin{proof}{} see the proof syntax # Comments \comment{}{} item can be the label of an invariant, a progress property, an event or a variable's name. The comment will be attached to the item in the generated summaries.
In machines and theories ...