Specification-forms
Forms of specifications handled by certain APT transformations.
Certain APT transformations operate on specifications
that are shallow pop-refinement predicates
as described in the `Specifications and Refinements' design notes, which use this notation. Currently these second-order predicates
must be expressed using SOFT.
In the future, the transformations may be extended
to operate on second-order predicates
expressed using the built-in apply$.
In this manual page,
we define and name certain specific forms of such SOFT specifications.
In the `Specifications and Refinements' design notes, these forms are shown
in Section `Some Shallow Pop-Refinement Specification Forms'.
APT transformations that operate on these forms
reference this manual page from their user documentation pages,
along with a designation of the form.
Pre/Post-Condition
This form is denoted by PP in the `Specifications and Refinements' design notes.
A specification of this form is a SOFT quantifier function
(see `Classification' section in soft::defsoft)
that has no parameters,
that depends on one function variable (call it ?f),
and whose body has the form
(forall (x1 ... xn)
(implies (pre x1 ... xn)
(post x1 ... xn (?f x1 ... xn))))where n is 1 or more,
implies may be impliez instead,
pre is a precondition predicate, and
post is a postcondition predicate.
Note that ?f returns a single result (not mv),
because SOFT function variables currently always do.
This is a typical specification consisting of
a precondition on the inputs and
a postcondition on the output (and inputs).
In the `Specifications and Refinements' design notes,
the specification is denoted by S,
?f is denoted by f,
x1, ..., xn are denoted by a single x
(the generalization to multiple variable is obvious),
pre is denoted by \Phi, and
post is denoted by \Psi.
Input/Output Relation
This form is denoted by Rf in the `Specifications and Refinements' design notes.
A specification of this form is a SOFT quantifier function
(see `Classification' section in soft::defsoft)
that has no parameters,
that depends on one function variable (call it ?f),
and whose body has the form
(forall (x1 ... xn)
iorel<x1,...,xn,(?f x1 ... xn)>)where n is 1 or more,
iorel<...> is a term that depends on the quantified variables
and that contains a single occurrence of
a call of ?f on the quantified variables.
The predicate (lambda (x1 ... xn y) iorel<x1,...,xn,y>)
is a relation between the inputs x1, ..., xn
and the output y.
This is a more general form than the pre/post-condition form PP,
which it subsumes.
In the `Specifications and Refinements' design notes,
the specification is denoted by S,
?f is denoted by f,
x1, ..., xn are denoted by a single x
(the generalization to multiple variable is obvious), and
(lambda (x1 ... xn y) iorel<x1,...,xn>) is denoted by R.
Input/Output Relation with Selected Input and Modified Inputs
This form is denoted by Rf\alpha in the `Specifications and Refinements' design notes.
A specification of this form is a SOFT quantifier function
(see `Classification' section in soft::defsoft)
that has no parameters,
that depends on one function variable (call it ?f),
and whose body has the form
(forall (x x1 ... xn)
iorel<x,x1,...,xn,(?f x a1<x1,...,xn> ... am<x1,...,xn>)>)where n may be 0 and
iorel<...> is a term that depends on the quantified variables
and that contains a single occurrence of
a call of ?f of the form shown above,
where m may be 0 and
each aj<x1,...,xn> is a term that depends on x1, ..., xn
(and must not depend on x).
The variable x does not actually have to be
the first quantified variable in the list after forall
and the first argument of the call of ?f:
it may be anywhere in the list and in any argument position,
as it is identified in same way by the APT transformations;
to ease exposition, in the documentation pages of the APT transformations,
we assume that it is the first one, as shown above.
This form generalizes the plain input/output relation form Rf,
because some of the inputs (namely x1, ..., xn)
are modified to become the terms aj<x1,...,xn>
before ?f is applied to them;
in addition, one input (namely x) is selected
and not subjected to that modification.
Thus, the input/output relation
(lambda (x x1 ... xn y) iorel<x,x1,...,xn,y>)
is applied, as the output,
not to a call of ?f directly on
the inputs x, x1, ..., xn,
but to a call of ?f on
the inputs x, a1<x1,...,xn>, ..., am<x,x1,...,xn>.
When m is n and each aj<x1,...,xn> is xj,
this form is the same as the plain input/output form Rf.
In the `Specifications and Refinements' design notes,
the specification is denoted by S,
?f is denoted by f,
x is denoted by x,
x1, ..., xn are denoted by \overline{x},
a1<x1,...,xn>, ..., am<x1,...,xn> are denoted by
\overline{\alpha}(\overline{x}), and
(lambda (x x1 ... xn y) iorel<x,x1,...,xn,y>)
is denoted by R.
