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