OS X / Linux:

What you need to do

• Get Haskell Platform
• Get Z3
• Get the Literate Unit-B source
• Compiling the utilities package
• Compiling the Unit-B program
• Run the test suite

Getting a Haskell Platform

Download the Haskell platform at https://www.haskell.org/

Z3

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.

Git

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

Compiling the utilities

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 ..

Compiling the Literate Unit-B Binaries

> cabal install

Compiling and Running the Tests

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 *
***********

Using Literate Unit-B

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.

Machine Syntax

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.

Proof Syntax

In machines and theories ...

Refinement of Progress Properties

Expression Syntax

Documentation Generation