Home | • | Intro | • | Wiki | • | Docs | • | FAQ | • | Download | • | Bugs | • | • | FM Tools |
---|

The command `abstract` implements an abstract compiler for PVS
assertions based on boolean abstractions. Given a state type
`STATE` defined as a record type and a set of state predicates
`(pred_1 ... pred_k)`, an abstract state type `ABS_STATE`
is defined. It consists of a record type with k boolean components and the
remaining components of the `STATE` that are not referenced in the
predicates `(pred_1 ... pred_k)`. The abstraction command
translates any PVS assertion over variables of type `STATE` to a
stronger assertion over variables of type `ABS_STATE`.

Syntax: `(abstract (pred_1 ... pred_k) &optional cases-rewrite?
[T] exclusive? proof-counter)`

**Effect**: The abstract command creates a new subgoal where the
selected formulae are translated using the abstract compiler defined by a
list of predicates. The command abstract rewrites all definitions,
including constant definitions such as the temporal operator of the logic
CTL. It then invokes the basic command abs-simp which implements the
abstract compiler. The command abs-simp assumes that all definitions have
been rewritten.

The list `(pred_1 ... pred_k)` is a list of state predicates of
the form ` lambda(s:state):P(s)`, where `P(s)` is any
predicate expressible in the PVS assertions language.

The parameter cases-rewrite? can be set to nil to avoid rewriting and simplification within unresolved selections within CASES expressions for the sake of efficiency.

The parameter exclusive? indicates weather the abstraction predicates are exclusive. This allows a more efficient computation of the abstraction.

The parameter proof-counter indicates the maximal number of calls to the decision procedure when abstracting each atom of the sequent. Any number allows to compute a faithful abstraction. However, it is preferable that the number is at least equal twice the length of the list of predicates.

**errors**: There are mainly two reasons for which the command can
not be applied:

- The first one is when one of the predicates does not satisfy the
condition given in section In this case the original goal is returned.
- P is not a predicate.
- Predicate P has free variables.
- State predicates have different domains.

- The second reason is when one of the selected formula contains variables which are not of type state. In this case the original goal is also returned.

The current use of the command `abstract` consists in using the
following proof strategy:

(defstep abstract-and-mc (list-state-predicates) (try (abstract list-state-predicates) (musimp) (skip)) "abstract-and-mc" "Interpret using boolean abstraction and prove by model-checking!")

The proof strategy applies successively the command `abstract`
and the command `musimp`, only if the command abstract produces a
modified subgoal. Otherwise the proof strategy has no effect.

**Example**: Consider the following state type: ` state : TYPE
[# pc : control ; y1,y2: nat #]` where control is an enumerated type
` control : TYPE = {idle, wait, enter, exit}` Consider a boolean
abstraction defined with the predicate ` lamda(s:state):
y1(s)=y2(s)` This defines the abstract state type ` abs_state :
TYPE [# pc : control; B_1 : boolean #] `

The assertion ` pc(state1)= idle and state2= state1 with [ pc :=
wait ; y1 := y2(state1)+1 ]` is abstracted to `
idle?(pc(abs_state1)) and pc(abs_state2)=wait and not
B_1(abs_state_2)`

**References**:
Abstract and Model Check while you prove by Hassen Saidi and Natarajan
Shankar describes the implementation of the abstraction command. This is
in the proceedings of the International Conference on Computer-Aided
Verification (CAV99), Trento, Italy, Jul 7-10, 1999.

Home | • | Intro | • | Wiki | • | Docs | • | FAQ | • | Download | • | Bugs | • | • | FM Tools |
---|

*
Last modified: Thu 17 May 2007 17:21 PDT
Maintainer: Sam Owre
*