From behavioural to structural properties:
A tool web interface
The translator allows behavioural control-flow properties of programs
to be transformed into equivalent sets of structural ones.
The specification language is the fragment of the modal mu-calculus
with boxes and greatest fixed points only.
The theory behind the translator is presented in the following
technical report.
More background and related work can be found at the
CVPP project web page.
Property and interface grammar
|
Atomic proposition
|
ap ::=
|
r | ff | tt | meth
|
|
Box label
|
l ::=
|
tau | meth call meth | meth ret meth
|
|
Property
|
phi ::=
|
ap | not ap | (phi) | phi /\ phi | phi \/ phi | [l]phi | prop_var | nu prop_var . phi
|
where meth is a string starting with a lower case, while prop_var is a string starting with an upper case.
Interfaces are given as a list of method names, separated by spaces only.
Example:
Property: nu X. ([a call b] ff) /\ ([tau] X) /\ ([a call a] X) /\ ([a ret a] X)
Interface: a b
Enter a behavioural property and an interface of provided methods: