Next: A Symbolic Verification Procedure
Up: An Assertional Language for
Previous: An Assertional Language for
In order to finitely represent the generators of an upward
closed set of configurations, we use a rich assertional language
based on the notion of constrained configurations, i.e.
multisets of (non ground) atomic formulas annotated with
constraints.
Let
be an
specification,
with
.
A constrained configuration is a multiset of atomic formulas
over and , annotated with a constraint, having the form
where
,
is a satisfiable
constraint, and
are distinct variables in
.
The set of ground instances of a constrained configuration can be
defined as follows.
Let
be an
specification,
and
a constrained configuration. The set of ground instances
of
is defined as
As an example, let be the constrained configuration
.
Then, if LC-constraints are interpreted over non-negative integers
contains
configurations like
,
, etc.
The previous definition can be extended to sets of constrained configurations
(denoted
) in the natural way:
Following the intuition we explained in the previous section,
instead of taking the set of instances as flat
denotation of a set of constrained configurations ,
we choose the following rich denotation.
Let
be an
specification, and a set of
constrained configurations (with distinct variables from
each other). The rich denotation of , denoted
,
is given by the upward closure of the set of its ground instances,
i.e.
Next: A Symbolic Verification Procedure
Up: An Assertional Language for
Previous: An Assertional Language for
Giorgio Delzanno
2003-02-03