invariant

The invariant statement specifies an invariant.

Syntax

The syntax of an invariant statement is as follows:

 invariant name { expression; } [in (state₁,state₂...state_n)]

The name specifies an invariant's name. The expression here must be a boolean expression. An invariant statement may explicitly specify a set of nodes, each node _i must be a defined node (with normal modifier).

Scope

An invariant can only be defined before the goal section.

Semantics

By default, an invariant must hold for all possible transitions in a graph. This means that, an invariant must be established in any transition in a graph. However, an invariant may not hold inside a node during the computation. When a specification contains an invariant, the compiler tries to discover counter-examples (depending on whether it is a check or enumerate statement) that will break invariant(s). There are two ways of using an invariant statement:

If an invariant statement without using an in clause, then this means that the invariant must hold for all possible transitions in a graph. This is useful for verifying if a property holds for every state. Cyclone ensures to discover a counter-example (breaking invariant) if there is any.
If an invariant statement that uses an in clause to specify a list of nodes, then this means that the invariant must hold in those specified nodes. This is useful for verifying if a property holds only for a subset of states (nodes) . Cyclone ensures to discover a counter-example (breaking invariant) in these states if there is any.

Example 1.

...

  normal node S1 {

  x -= a;

  x = (y-x)*2 ;

...

 invariant  positive { x >= 0; }

 goal {  check for 1,2,3,4,5 reach  (S0) }

The positive invariant specifies the variable x must be greater or equal to 0. This invariant must hold for every transition. However, it may not hold during the computation. Hence, this invariant could be violated at the statement x-=a;. But it must be established after computing statement x=(y-x)*2;

The goal section here asks Cyclone to discover whether there exists a path (with path length 1,2,3,4,5) that can break invariant positive and each path must reach node S0.

Example 2.

 invariant  safety { x + y + z <= max; } in (S0,S2,S3)

 goal {  check for 5 }

The goal section here asks Cyclone to discover whether there exists a path (with path length 5) that can break invariant safety in nodes S0, S2 or S3.

< Back