User Manual

1 Introduction

The SPADE Automatic Simplifier is a standalone tool which supersedes the simplifier which used to be built into the SPADE Verification-Condition Generator (VCG). It performs many of the simplifications carried out by the earlier VCG simplifier for verification conditions, but also includes rules for the simplification of FDL’s compound data types, such as arrays, records, sets and sequences.

The SPADE Automatic Simplifier (SAS) reads the .vcg file generated by either the SPADE VCG or the SPARK[1] Examiner with Verification-Condition Generator, plus the .fdl file for its data declarations. Where proof-rule files (with the same filename, but extension .rls or .rlu) are present, these are also read and utilised by the SAS. The SAS can be applied to any .vcg file. The tool detects which sort of file contents to expect either by scanning the heading text or, in the case of output generated by the Examiner, by the extension (.vcg for VCs); it is therefore important that you do not edit a .vcg file to modify its format in any way if you intend to submit it to the SAS for simplification. The SAS generates two output files: a .siv file containing the simplified VCs, and a .slg file which contains a log giving information about the simplifications performed by the Simplifier.

In the remaining sections of this document, we offer some general remarks on simplification, then provide a more detailed account of the steps performed by the Simplifier in attempting to simplify a .vcg file; this is followed by some examples and a description for the more advanced user of the command-line switches which may be used to control the behaviour of the Simplifier, should this prove desirable for more complex formulae. We then provide some notes on the format of the .slg log file, and the various messages which can appear in the simplification log, followed a definition of the proof-rule language which may be used to define additional user-defined proof rules for use by the Simplifier.

2 A note about simplification

When is one expression “simpler” than another? In certain circumstances, it is “obvious” which expression is simpler, e.g. few people would seriously argue that 3+4 is simpler than 7, or that x+1=2 is simpler than x=1. Many people would agree that 4*x is simpler than (x+(x+x))+x, or even x+x+x+x, even though 4*x uses a different operation — multiplication as shorthand for repeated addition. But is a*m+(b*n-d)=0 simpler than d=a*m+b*n? This is debatable; yet the former expression is the simplified form of the latter, according to the expression simplification algorithm which used to be built into the SPADE VCG.

An approach that is typically taken in constructing an expression simplifier is to determine some partial ordering over expressions, which may indicate which of two expressions is the simpler. A drawback, however, is that this ordering may be counter-intuitive in some circumstances, as the example of the preceding paragraph suggests.

The simplifier which was formerly built into the SPADE VCG attempted to simplify expressions by reduction to a canonical form. This was its single strategy, using various equivalence-preserving transformations to achieve the necessary rewriting, and it can be remarkably successful for a class of expressions. However, one had to take this simplifier on trust, which was sometimes difficult where the simplified expression appeared quite dissimilar to the original.

In order to provide a more comprehensible simplification tool, various components from the existing SPADE Proof Checker have been assembled, together with some additional tools based on technology in the former SPADE VCG’s simplifier, into this standalone Automatic Simplifier. There is no guarantee that the transformations performed by the new Simplifier will always result in intuitively simpler expressions, but rewriting to a canonical form - which often results in radically different expressions that are unrecognisable by the user - is avoided unless it appears to yield a notably “smaller” expression. In addition, the log produced by the SAS can also be inspected, to gain some understanding of the steps performed by the Simplifier for each VC, which makes it easier to inspect and understand the results of simplification.

3 Actions performed in simplification

At the outermost level, the Simplifier reads a .vcg file and simplifies it, thereby creating an output .siv file.

The simplification itself is performed on each VC in turn, and as each is read it can optionally be echoed to the user’s screen together with a log of actions, to display progress. The fundamental algorithm employed in simplifying each VC is:

{1} scalar-constants-substitutions-in-rules[2];

{2} restructure-expressions;

{3} simplify-expressions;

{4} perform-global-logical-simplifications;

{5} try-to-prove-conclusions & exit if successful;

{6} constant-substitution-phase-1;

try-to-prove-conclusions & exit if successful; -- repeat of step 5

{7} constant-substitution-phase-2;

{8} construct-standard-forms;

try-to-prove-conclusions & exit if successful; -- repeat of step 5

{9} look-for-contradiction & exit if successful;

{10} perform-expression-reduction;

perform-global-logical-simplifications again; -- repeat of step 4

additional-integer-modulus-simplifications;

try-to-prove-conclusions & exit if successful; -- repeat of step 5

{11} try-proof-framing;

{12} apply-user-defined-proof-rules.

We shall give an overview of each of these processes in the following sections.

3.1 Scalar constants substitution into rules

Within the .rls file generated for a subprogram by the Examiner, there are both simple rules (which give the value of scalar constants, e.g. natural__first may_be_replaced_by 0) and more complex rules, which may make use of such scalar constants. Within the latter category, there may be rules which specify values for, or constraints upon, the values associated with composite constants. For example, we might see a rule such as

mysubprogram_rule(5): natural__first <= element(c, [I])

may_be_deduced_from [1 <= I, I <= 10].

which states that all elements of the constant array c are bounded below by natural__first.

In its early processing, the Simplifier will eliminate such named scalar constants with more complex rules automatically, as a ‘one-off’ operation on the rules (rather than repeat the substitution once for each VC in which the rule is used). In doing so, the instance of natural__first in the above rule will be replaced by 0, so that the rule becomes

mysubprogram_rule(5): 0 <= element(c, [I])

may_be_deduced_from [1 <= I, I <= 10].

This latter form may then be used in a later proof phase to prove conclusions which require a lower bound on expressions involving elements of the composite constant c.

3.2 Expression restructuring

This step occurs on reading the VC into the Simplifier. It performs some conversions where necessary from the FDL syntax generated by the SPADE VCG (or Examiner with Verification-Condition Generator) to that used by the SPADE Proof Checker, as documented in the SPADE Proof Checker User Manual. These changes affect set and sequence constructors and the set operators for union, intersection, difference and subset comparison. The changes made (where x and y are of some set type) are:

FDL syntax	Restructured syntax
Seqtype [e1,...,en]	[e1,...,en]
Settype [e1,...,en]	set [e1,...,en]
x + y	x \/ y
x * y	x /\ y
x - y	x \ y
x <= y	x subset_of y
x >= y	y subset_of x
x < y	x strict_subset_of y
x > y	y strict_subset_of x

This rewriting enables components from the SPADE Proof Checker’s simplification tools to be used in the Simplifier without modification, and reduces the overloading of the operators +, -, * and the relational operators.

3.3 Expression simplification

When expression simplification is enabled (the default), each expression is simplified using a simplification strategy which works from the leaves of the expression-tree upwards. It is not possible to give all of the rules used by the Simplifier, as there are many of them, but the following examples give a flavour of the rules:

Expression	Simplifies to
not true	False
not (not X)	X
true and X	X
X or X	X
X -> false	(not X)
X <-> X	True
X + 0	X
X * 0	0
X * 1	X
X - X	0
X div 1	X
X + N - N	X
A + B	C (where A,B,C are integers and C=A+B)
X /\ X	X
X \/ X	X
X \ X	set [] (the empty set)
X @ []	X
first([X,...])	X
element(update(A,[I],X),[I])	X
fld_f(upf_g(R,X))	fld_f(R) (fields f and g are distinct)

Note that the expression simplifier does not do any reordering of the expression, however: a+b simplifies to a+b, and b+a to b+a, so they do not simplify to the same expression. Thus the expression simplifier is a fairly weak proof strategy for proving the equivalence of two expressions, but is relatively fast (so it can be applied to quite large expressions) and gives results which are virtually guaranteed to be “simpler” (though not necessarily “simplest”).

3.4 Global logical simplifications

This step may change the hypotheses and conclusions of the current VC, by moving negation inwards as far as possible, splitting up conjunctions and adding new consequents. Moving logical negation inwards as far as possible can change the structure of a hypothesis or conclusion. For example, given

H1: not (a or (not (b or c) or d))

if we move negation inwards as far as possible (using DeMorgan’s laws) we get

H1: not a and (b or c) and not d .

This is now a conjunction (and); global logical simplification splits up such conjunctions (in both hypotheses and conclusions) into component pieces; so the above becomes:

H1: not a

H2: b or c

H3: not d .

One final global logical simplification performed is to look for hypotheses which consist of an implication (or equivalence — which is regarded as a pair of implications for this purpose) and attempt to establish that the left-hand side of the implication follows from the current hypotheses; if this can be done, the right-hand side can be added as a new hypothesis. Thus, given

H1: a -> b

for instance, if we also have a hypothesis such as

H2: a

which establishes the left-hand side, a new hypothesis

H3: b

is added.

3.5 Proof of conclusions

The strategy used to attempt to prove the conclusions of the current VC is similar to the built-in inference engine of the SPADE Proof Checker. Thus, conclusions which the inference engine can deduce from the existing hypotheses are proved, and withdrawn from the VC; if all the conclusions can be inferred in this way, the whole VC is proved and its simplified form is then merely true. In looking for a proof, the inference engine will also make use of any standard forms; and the proof records which hypotheses were used directly by the inference engine in establishing each conclusion which it proves.

3.6 Constant substitution phase 1

This step finds conclusions of the form “X >= Y” or “X <= Y” where one of X or Y is an identifier denoting an FDL constant that has a replacement rule allowing it to be replaced by a literal value. For all such conclusions, the identifier is replaced by the corresponding literal in all hypotheses and conclusions.

This phase is immediately followed by an attempt to infer conclusions. If all conclusions can be inferred at this point, then the VC is reduced to “true” and no further action is taken.

3.7 Constant substitution phase 2

This step applies all remaining constant replacement rules (that appear in the RLS file generated by the Examiner.) For each replacement rule, the constant identifier is replaced by the corresponding literal in all hypotheses and conclusions.

3.8 Construction of standard forms

For each sufficiently “small” (with respect to a “complexity limit”) hypothesis and conclusion, the Simplifier constructs a “standard” form, which is similar to what would be returned by the SPADE Proof Checker’s expression standardiser (via the “standardise” command). Such standard forms are only constructed if standardisation is enabled (the default), however. The standard form may radically change an expression’s structure, multiplying out terms such as (a+b)*(d+c), collecting “like” terms and ordering sums of products lexicographically. Standardisation is thus more powerful (and, in consequence, more CPU-intensive — hence the complexity limit on its application) than the simplification of section 3.3 above, since for instance both

(a + b) * (d + c) - a * (3 - 1) * d

and

c * (b + a) + 0 - d * (a - b)

have the same standard form:

a * c - a * d + b * c + b * d .

There is thus a class of expressions which are demonstrably equivalent via standardisation, but not via the expression simplifier. This stage constructs these standard forms, together with “semi-standard” forms for relational expressions, in which each side of the relational operator is standardised in isolation; these standardised forms may be useful in later stages, or may be significantly “simpler” with respect to the complexity metric which we employ for comparison purposes, in which case the standard form may be output as the simplified form of the hypothesis/conclusion in question.

3.9 Search for a contradiction

If the inference engine cannot eliminate all of the VC’s conclusions, the next strategy (if it is enabled — the default) is to search for a contradiction in the hypotheses of the VC. If a contradiction can be established, then the execution path through the source code to which this VC corresponds is non-traversable (provided the assertion at the top of the path holds: this assumption is discharged by proof of the VCs for paths which terminate at this assertion), and the formula as a whole is true, since

false -> X

is true in our classical logic for any logical expression X. Thus, if we can establish a contradiction, we can eliminate the VC entirely from further consideration.

The search for a contradiction takes place in five phases:

1 If we have a hypothesis false (or whose standard form is false), we have established a contradiction.

2 If not, we look for mutually exclusive hypotheses: for each hypothesis P, we attempt to infer (not P), possibly using standardisation to help.

3 If not, we try to find a variable with an empty range. Thus, if we have a hypothesis which constrains a variable X in some way (e.g. X>3), we try to find one or more other hypotheses which constrain X in a different (and contradictory) way. Thus, for X>3, if we can also find that X<b and prove that b<=3, we have a contradiction, as X is constrained to an empty range of values.

4 If not, and provided standardisation is enabled (the default), the Simplifier constructs a collection of joins between two hypotheses at a time (and then further joins of the join facts, etc). A join is essentially formed by “adding” (or “subtracting”) two relational expressions in a sound way, e.g. given

x - y = 0 —(a)

y - z = 0 —(b)

we can form the join which is 1*(a)+1*(b), giving (after standardisation)

x - z = 0 .

Of course, we can form arbitrary joins of j*(a)+k*(b), but it is only when j=k that we get a cancellation for the above two formulae, and values other than 1 are not necessary as they merely introduce additional numeric factors (e.g. 2*x-2*z=0). The Simplifier therefore looks only for joins which give rise to at least one term cancellation, and calculates the multipliers in such a way that unnecessary numeric multiples are avoided (an application for the GCD algorithm!). The Simplifier keeps constructing joins until one of the following conditions is met:

· a contradiction is established (a join standardises to false); or

· no more new joins can be found; or

· the depth limit is reached; or

· the inference limit is reached.

The latter two limits control the amount of effort put into the search; they are fixed in the demonstration version of the Simplifier. The depth of a new join is 1 if both its parents are hypotheses, or n+1 if one or more of its parents are themselves join facts, and n is the depth of the deeper parent. Thus, with a depth limit of 5 (the default), join facts constructed from up to 32 hypotheses (2**5) may be formed if this is possible. The other limit, the inference limit, determines the maximum number of joins which may be constructed (including repetitions, constructed via different routes) without finding a contradiction, before the Simplifier gives up and proceeds to step (5).

5 If steps (1)-(4) do not establish a contradiction within the hypotheses, the Simplifier looks for equality facts (those of the form X=Y, for expressions X and Y) and/or hypotheses of the form Z or not Z, where Z is a boolean variable (or constant). For X=Y, the strategy of substituting Y for X (or vice versa) throughout the VC is tried; the resulting new hypotheses are standardised and, if any yield false, a contradiction has been established. For hypotheses of the form Z (or not Z), all occurrences of Z in the VC are replaced by true (or false) and, again, a contradiction is sought via standardisation.

If none of steps (1)-(5) above discovers a contradiction, the next step is to try to simplify the existing VC further by other means.

3.10 Expression reduction

The expression-reduction step attempts to throw away redundant hypotheses or parts of hypotheses, and reduce the number of apparently independent variables occurring in the VC by substitution. This step is skipped if a contradiction has already been established via the preceding processes, or if all of the conclusions of the VC have already been proved, in which case the hypotheses too may be discarded. Expression reduction is performed in eight stages:

1 If any hypothesis (or its standard form) is true, the hypothesis may be discarded.

2 If there are any disjunction hypotheses (A or B) in which one component can be inferred to hold (e.g. if we can infer A from the existing hypotheses), then the disjunction can be collapsed down to true and thus eliminated.

3 If there are any repeated hypotheses, the repetitions may be discarded so that only one copy of the hypothesis is retained.

4 If any range-subsumptions are found among the hypotheses (e.g. given both x>0 and x>1, the former is superfluous), the subsumed hypothesis or hypotheses can be eliminated.

5 If there are any complementary pair disjunctions (e.g. x>0 or x<3) in which one part of the disjunction is a consequence of the negation of the other parts (thus, for the example given, not x>0 -> x<3 is true), such hypotheses can also be eliminated.

6 If there are any implication hypotheses (regarding an equivalence as a pair of implications), the Simplifier uses the inference engine to try to satisfy the left-hand side: success allows the hypothesis (A -> B) to be reduced to its consequent (B).

7 Redundant hypotheses are also hunted with the join mechanism discussed in the preceding section. Using the existing hypotheses and join facts (limited to those of depth 1 currently, so hypotheses which are a consequence of three or more other hypotheses will not be eliminated by this process), the negation of each relational expression hypothesis is formed and joined with the other hypotheses and their join facts in a search for a contradiction; if one is found, the hypothesis under investigation is redundant (since, if (not X) forms a contradiction with Y, then Y -> X, so X is irrelevant given Y) and can be discarded.

8 Finally, if substitution elimination is enabled (the default), the Simplifier looks for hypotheses of the form V=E (or E=V), where V is an identifier declared to be a variable in the FDL declarations that were read in, and E is an expression which does not contain any references to V. For each such hypothesis found in turn, the Simplifier replaces all occurrences of V in the VC by E, then discards the hypothesis V=E. In general, E will be a larger expression than V, but these substitutions reduce the number of apparently independent variables occurring in the VC and may also allow other simplifications to be performed. For the purposes of this step, proof rules in a proof-rule file (of the same filename, but with extension .rls) are treated as implicit equalities; a rule of the form c may_be_replaced_by v, where c is an identifier and v a value expression, is used to eliminate all occurrences of c and replace each one by the corresponding value, v.

After this reduction, some additional strategies are attempted, including some which attempt to derive the greatest lower bound and least upper bound on each expression and subexpression with the aim of discharging some more complex range constraints that may still be remaining at this stage. The VC is then restructured once more (a repetition of step 3, since the preceding simplifications may result in the opportunity for further global simplifications) and additional simplification of expressions involving the integer modulus is attempted. (For example, x mod 256 will be replaced by x if it can be established that 0<=x<=255 holds.) A further attempt is then made to eliminate the remaining unproved conclusions, given the simplifications and modifications that have occurred. If there are still unproven conclusions after this, an attempt is made to eliminate these via proof-framing, as described in the next section.

3.11 Proof framing

If there are still conclusions remaining to be proved by this stage, the Simplifier inspects each of the remaining conclusions in turn to look for three common patterns:

· universal quantification: for_all(x:t, p(x));

· implication: p -> q;

· array object updates: element(update(a, [i], x), [j]) or update(update(a, [i], x), [j], y).

If any of these elements are present, the Simplifier uses a “proof-framing” approach to break the conclusion down into subgoals, as follows.

1 If the conclusion C is of the form for_all(x:t, p(x)),

a create a new unique identifier x’,

b declare it to be of type t,

c enter a new proof-frame in which existing conclusions are (temporarily) withdrawn and a new conclusion C’: p(x’) [possibly entailing some further simplification, and splitting up if the formula is a conjunction or implication] becomes the goal.

2 If the conclusion C is of the form p -> q,

a enter a new proof-frame in which existing conclusions are (temporarily) withdrawn and a new conclusion C’: q becomes the goal,

b add new hypotheses H’: p (splitting up conjunctions in doing so).

3 If the conclusion C contains any element(update(_,[i],_),[j]) or update(update(_,_[i]_),[j],_) patterns for which neither i=j nor i<>j can be inferred automatically by the inference engine,

a enter a new proof-frame in which existing conclusions are (temporarily) withdrawn and the only subgoal conclusion is C,

b add a new H: i=j and attempt to prove the conclusion,

c if this succeeds, restart the proof framing but now with H: i<>j instead, and try to prove the conclusion.

This proof-framing approach can itself be applied recursively to the subgoals generated in the search for a proof. For example, consider the VC

H1: 1 <= n

H2: n <= 10

H3: 0 <= x

H4: x <= 100

H5: for_all(i:integer, 1 <= i and i <= 10 -> 0 <= element(a, [i]) and element(a, [i]) <= 100)

-->

C1: for_all(i:integer, 1 <= i and i <= 10 -> 0 <= element(update(a, [n], x), [i]) and

element(update(a, [n], x), [i]) <= 100.

In applying the proof-framing strategies to C1, the Simplifier spots that the conclusion is universally-quantified, and so applies strategy 1, converting C1 into a new subgoal:

C1: 1 <=int_i_1 and int_i_1 <= 10 -> 0 <= element(update(a, [n], x), [int_i_1]) and

element(update(a, [n], x), [int_i_1]) <= 100.

Next, it spots the new subgoal C1 is an implication formula, so it applies strategy 2, giving two new hypotheses:

H6: 1 <= int_i_1

H7: int_i_1 <= 10

and a revised subgoal formula C1:

C1: 0 <= element(update(a, [n], x), [int_i_1]) and

element(update(a, [n], x), [int_i_1]) <= 100.

Next, the Simplifier observes that there is an array access of an update(...) expression. Since it cannot prove either that n=int_i_1 or that n<>int_i_1, proof-framing strategy 3 is appropriate and can be tried. This yields a proof by cases. In case 1, we gain a new hypothesis

H8: n = int_i_1

and, because n=int_i_1 in this case, the element(update(...),...) expression simplifies to x, giving a new subgoal

C1: 0 <= x and x <= 100

which can be proved from hypotheses H3 and H4, completing the proof for case 1.

For case 2, we instead have a new hypothesis

H8: n <> int_i_1

and, because n<>int_i_1 in this case, the element(update(...),...) expression simplifies to element(a, [int_i_1]), giving a new subgoal

C1: 0 <= element(a, [int_i_1]) and element(a, [int_i_1]) <= 100.

This subgoal conclusion can be proved from H5 (a universally-quantified hypothesis, which says all elements of a within the index range 1..10 are themselves in the range 0..100), given that H6 and H7 tell us that int_i_1 is within the valid index range 1..10. This therefore completes the proof for case 2 also, and as those are the only two cases to consider, we’ve completed a proof of our original conclusion, using all three proof-framing strategies along the way.

In this way, the proof-framing code within the Simplifier mimics some common proof techniques used within the SPADE Proof Checker, automating the proofs of such formulae in a significant number of cases.

3.12 Application of user-defined rules

If, after applying all of the preceding phases, there are still unproven conclusions within the current VC, the Simplifier will check to see if any user-defined rules have been read in. (Refer to section 7 for details of the naming conventions for user-defined proof-rule files, the syntax and semantics of these proof rules and on how pattern-matching against the rules, and satisfaction of side-conditions, is achieved.) Any user-defined rules which have been read in are listed at the beginning of the .slg file, along with any syntax errors found in those rules. This listing is in the form:

RRS The following user defined rule files have been read:

&&& control.rlu.

&&& transfer.rlu.

STX The rule files contained the following syntax errors:

(any syntax errors found will be listed here)

SEM No semantic checks are performed on the rules.

The warning above serves as a reminder that great care must be taken with user-defined rules as an incorrect rule could enable the Simplifier to prove a conclusion which is false.

If one or more user-defined proof rules has been read in, the Simplifier will attempt at this stage to make use of these to prove each of the remaining conclusions in turn, in its final attempt to complete the proof of the current VC.

To apply the user-defined proof rules, the Simplifier tries the following, in order. (At each stage as the use of the user-defined proof rules proceeds, the Simplifier also repeatedly checks to see if all the remaining conclusions have now been proved and, if so, exits the proof of the VC and records its overall success in doing so.)

1 First, for each remaining conclusion, the Simplifier attempts to find an inference rule which pattern-matches with the conclusion. If it can find such a match, it will attempt to satisfy the resulting list of conditions associated with the rule and, if is successful in satisfying all of these, it will record the conclusion as proved and record the proof in the log file.

2 Next, for each remaining conclusion, the Simplifier attempts to find a rewrite rule which pattern-matches against the conclusion or one of its subexpressions. For each such match it finds, it will attempt to satisfy the resulting list of conditions associated with the rule. If any of these matches is successful, and if the rewritten conclusion can also be seen to follow from the hypotheses as a result of the rewrite, then the conclusion is recorded as proved and the proof log updated accordingly. (In this way, steps 1 and 2 are ‘subgoaling’, or performing a ‘backward search’ on the existing goal (conclusion), attempting to apply a rule to infer it from, or rewrite it to, facts in the existing hypotheses.)

3 Next, the Simplifier attempts to augment the existing hypotheses of the VC, adding extra facts by using the rewrite rules. It does this by pattern-matching each of the rewrite rules against the existing hypotheses, and attempting to satisfy the resulting list of conditions associated with the rule-match. If all of the list of conditions is satisfied for a match, the resulting rewritten hypothesis is recorded as an extra fact, for use in subsequent steps. (In this way, step 3 is ‘forwardchaining’, or performing a ‘forward search’ on the existing hypotheses, attempting to apply a rule to infer additional facts to add to the set of facts already present in the hypotheses.)

4 Next, the Simplifier attempts to establish, for each remaining conclusion, if it can be inferred from the augmented set of hypotheses (that is, the original ones, plus the new facts derived as a result of the forwardchaining in step 3), and records this fact if so.

Steps 1 to 4 are then repeated a further time, and then steps 1 and 2 once more. In this way, reasoning consisting of the application of a number of rewrite rules may be ‘chained’ together to construct a proof for a conclusion formula, and the proof log will record the additional facts that were added and the rule substitutions that occurred to construct the proof, detailing also the rule instantiation and how each of the conditions in the rule’s conditions list was satisfied.

The finite reapplication of steps 1 to 4, as described above, ensures that this process will terminate. However, if the user defines a large number of proof rules, the step may nevertheless take a significant amount of time to terminate, since each possible rule-match will be explored as the search for a proof is undertaken. Furthermore, it should be noted that this algorithm is not guaranteed to find a proof consisting of an arbitrarily long number of inference and rewrite rule applications: after experimentation, this ‘hard-wired’ limit has been settled on as offering a reasonable degree of automation and allowing users to experiment with the definition and use of their own proof rules, without the need for additional safeguards against non-termination. (N.B. The strategy is likely to be revised in the light of further experience as a result of using this new facility, once sufficient experience has been gained.)

If any of the conclusions for a VC have been proved with the aid of user-defined rules then a summary of the application of user-defined rules for the VC is output at the end of the log for the VC in the .slg file. This summary is in the following form:

VCN 3: Summary of user rule application. (VC number)

FIL control.rlu (rule file name)

RUL rule(1) (rule number)

CON 1, 2, 4 (conclusions proved using this rule)

RUL rule(2)

CON 2, 3

HYP 44 (hypotheses created using this rule)

An overall summary of the application of user-defined rules for all VCs is output at the end of the .slg file (if any user-defined rules were actually applied in order to prove any conclusions). This summary is in the following form:

OVR Overall summary of VCs using user rules.

FIL control.rlu (rule file name)

RUL rule(1) (rule number)

VCS 7, 9, 22. (VCs for which this rule was applied)

FIL transfer.rlu

RUL xyz(1)

VCS 12, 14, 16

4 Examples

4.1 Verification conditions

Fig.1(a-c) on the following pages lists some verification conditions for an example called DIVIDE, together with the Simplifier output for these verification conditions. Fig.1(a) shows the verification conditions before simplification, while Fig.1(b) lists the .siv output file which contains the simplified verification conditions and Fig.1(c) shows the .slg log file generated by the Simplifier as a record of the simplification actions performed.

The following set of figures, Fig.2(a-c) provides similar output files for example EXTGCD. Notice that all of these figures were generated using the Simplifier’s default settings: no command-line switches (discussed in the following section) were used to control the Simplifier in any way.

*******************************************************

Semantic Analysis of SPARK Text

SPARK95 Examiner with VC Generator, Release 7.2 / 12.04

Altran Praxis Limited, Bath, England

*******************************************************

DATE : 08-DEC-2004 14:13:34.37

procedure P.Divide

For path(s) from start to assertion of line 18:

procedure_divide_1.

H1: m >= 0 .

H2: n > 0 .

C1: m = 0 * n + m .

C2: m >= 0 .

C3: n > 0 .

For path(s) from assertion of line 18 to assertion of line 18:

procedure_divide_2.

H1: m = q1 * n + r1 .

H2: r1 >= 0 .

H3: n > 0 .

H4: not (r1 < n) .

C1: m = (q1 + 1) * n + (r1 - n) .

C2: r1 - n >= 0 .

C3: n > 0 .

For path(s) from assertion of line 18 to finish:

procedure_divide_3.

H1: m = q1 * n + r1 .

H2: r1 >= 0 .

H3: n > 0 .

H4: r1 < n .

C1: m = q1 * n + r1 .

C2: r1 >= 0 .

C3: r1 < n .

Fig.1(a): Verification conditions for the DIVIDE procedure

*******************************************************

Semantic Analysis of SPARK Text

SPARK95 Examiner with VC Generator, Release 7.2 / 12.04

Altran Praxis Limited, Bath, England

*******************************************************

CREATED 08-DEC-2004, 14:13:34 SIMPLIFIED 08-DEC-2004, 14:14:55

(Simplified by SPADE Simplifier, Version 2.17)

procedure P.Divide

For path(s) from start to assertion of line 18:

procedure_divide_1.

*** true . /* all conclusions proved */

For path(s) from assertion of line 18 to assertion of line 18:

procedure_divide_2.

*** true . /* all conclusions proved */

For path(s) from assertion of line 18 to finish:

procedure_divide_3.

*** true . /* all conclusions proved */

Fig.1(b): DIVIDE.siv simplified verification conditions

****************************************************

LOG OF SIMPLIFICATIONS PERFORMED BY SPADE SIMPLIFIER

PRAXIS HIS SPADE TOOL VERSION : 2.31

****************************************************

DATE : 02-MAY-2007 TIME : 14:14:53

@@@@@@@@@@ VC: procedure_divide_1. @@@@@@@@@@

%%% Simplified C1 on reading formula in, to give:

%%% C1: true

*** Proved C1: true

*** Proved C2: m >= 0

using hypothesis H1.

*** Proved C3: n > 0

using hypothesis H2.

*** PROVED VC.

@@@@@@@@@@ VC: procedure_divide_2. @@@@@@@@@@

>>> Restructured hypothesis H4 into:

>>> H4: n <= r1

*** Proved C1: m = (q1 + 1) * n + (r1 - n)

via its standard form, which is:

Std.Fm C1: m - n * q1 - r1 = 0

using hypothesis H1.

*** Proved C2: r1 - n >= 0

using hypothesis H4.

*** Proved C3: n > 0

using hypothesis H3.

*** PROVED VC.

@@@@@@@@@@ VC: procedure_divide_3. @@@@@@@@@@

*** Proved C1: m = q1 * n + r1

using hypothesis H1.

*** Proved C2: r1 >= 0

using hypothesis H2.

*** Proved C3: r1 < n

using hypothesis H4.

*** PROVED VC.

Fig.1(c): DIVIDE.slg simplification log

*******************************************************

Semantic Analysis of SPARK Text

SPARK95 Examiner with VC Generator, Release 7.2 / 12.04

Altran Praxis Limited, Bath, England

*******************************************************

DATE : 08-DEC-2004 13:55:00.92

procedure P.ExtGCD

For path(s) from start to assertion of line 22:

procedure_extgcd_1.

H1: true .

H2: n <> 0 .

C1: m > 0 .

C2: n >= 0 .

C3: 0 * m + 1 * n = n .

C4: 1 * m + 0 * n = m .

C5: gcd(m, n) = gcd(m, n) .

For path(s) from assertion of line 22 to assertion of line 22:

procedure_extgcd_2.

H1: c > 0 .

H2: d >= 0 .

H3: a1 * m + b1 * n = d .

H4: a2 * m + b2 * n = c .

H5: gcd(c, d) = gcd(m, n) .

H6: c - c div d * d <> 0 .

C1: d > 0 .

C2: c - c div d * d >= 0 .

C3: (a2 - c div d * a1) * m + (b2 - c div d * b1) * n =

c - c div d * d .

C4: a1 * m + b1 * n = d .

C5: gcd(d, c - c div d * d) = gcd(m, n) .

For path(s) from start to finish:

procedure_extgcd_3.

H1: true .

H2: not (n <> 0) .

C1: m = gcd(m, n) .

C2: m = 1 * m + 0 * n .

For path(s) from assertion of line 22 to finish:

procedure_extgcd_4.

H1: c > 0 .

H2: d >= 0 .

H3: a1 * m + b1 * n = d .

H4: a2 * m + b2 * n = c .

H5: gcd(c, d) = gcd(m, n) .

H6: not (c - c div d * d <> 0) .

C1: d = gcd(m, n) .

C2: d = a1 * m + b1 * n .

Fig.2(a): Verification conditions for procedure EXTGCD

*******************************************************

Semantic Analysis of SPARK Text

SPARK95 Examiner with VC Generator, Release 7.2 / 12.04

Altran Praxis Limited, Bath, England

*******************************************************

CREATED 08-DEC-2004, 13:55:00 SIMPLIFIED 08-DEC-2004, 13:55:42

(Simplified by SPADE Simplifier, Version 2.17)

procedure P.ExtGCD

For path(s) from start to assertion of line 22:

procedure_extgcd_1.

H1: n <> 0 .

C1: m > 0 .

C2: n >= 0 .

For path(s) from assertion of line 22 to assertion of line 22:

procedure_extgcd_2.

H1: a2 * m + b2 * n > 0 .

H2: a1 * m + b1 * n >= 0 .

H3: gcd(a2 * m + b2 * n, a1 * m + b1 * n) = gcd(m, n) .

H4: a2 * m + b2 * n - (a2 * m + b2 * n) div (a1 * m + b1 * n) *

(a1 * m + b1 * n) <> 0 .

C1: a1 * m + b1 * n > 0 .

C2: a2 * m + b2 * n - (a2 * m + b2 * n) div (a1 * m + b1 * n) *

(a1 * m + b1 * n) >= 0 .

C3: gcd(a1 * m + b1 * n, a2 * m + b2 * n - (a2 * m + b2 * n) div

(a1 * m + b1 * n) * (a1 * m + b1 * n)) = gcd(m, n) .

For path(s) from start to finish:

procedure_extgcd_3.

H1: true .

C1: m = gcd(m, 0) .

For path(s) from assertion of line 22 to finish:

procedure_extgcd_4.

H1: a2 * m + b2 * n > 0 .

H2: a1 * m + b1 * n >= 0 .

H3: gcd(a2 * m + b2 * n, a1 * m + b1 * n) = gcd(m, n) .

H4: a2 * m + b2 * n - (a2 * m + b2 * n) div (a1 * m + b1 * n) *

(a1 * m + b1 * n) = 0 .

C1: a1 * m + b1 * n = gcd(m, n) .

Fig.2(b): EXTGCD.siv simplified verification conditions

****************************************************

LOG OF SIMPLIFICATIONS PERFORMED BY SPADE SIMPLIFIER

PRAXIS HIS SPADE TOOL VERSION : 2.31

****************************************************

DATE : 02-MAY-2007 TIME : 13:55:41

@@@@@@@@@@ VC: procedure_extgcd_1. @@@@@@@@@@

%%% Simplified C3 on reading formula in, to give:

%%% C3: true

%%% Simplified C4 on reading formula in, to give:

%%% C4: true

%%% Simplified C5 on reading formula in, to give:

%%% C5: true

*** Proved C3: true

*** Proved C4: true

*** Proved C5: true

--- Eliminated hypothesis H1 (true-hypothesis).

@@@@@@@@@@ VC: procedure_extgcd_2. @@@@@@@@@@

*** Proved C4: a1 * m + b1 * n = d

using hypothesis H3.

-S- Eliminated hypothesis H3.

This was achieved by replacing all occurrences of d by:

a1 * m + b1 * n.

<S> New H2: a1 * m + b1 * n >= 0

<S> New H5: gcd(c, a1 * m + b1 * n) = gcd(m, n)

<S> New H6: c - c div (a1 * m + b1 * n) * (a1 * m + b1 * n) <> 0

<S> New C1: a1 * m + b1 * n > 0

<S> New C2: c - c div (a1 * m + b1 * n) * (a1 * m + b1 * n) >= 0

<S> New C3: (a2 - c div (a1 * m + b1 * n) * a1) * m + (b2 - c div

(a1 * m + b1 * n) * b1) * n = c - c div (a1 * m + b1 * n) *

(a1 * m + b1 * n)

<S> New C5: gcd(a1 * m + b1 * n, c - c div (a1 * m + b1 * n) * (a1 *

m + b1 * n)) = gcd(m, n)

-S- Eliminated hypothesis H4.

This was achieved by replacing all occurrences of c by:

a2 * m + b2 * n.

<S> New H1: a2 * m + b2 * n > 0

<S> New H5: gcd(a2 * m + b2 * n, a1 * m + b1 * n) = gcd(m, n)

<S> New H6: a2 * m + b2 * n - (a2 * m + b2 * n) div (a1 * m + b1 *

n) * (a1 * m + b1 * n) <> 0

<S> New C2: a2 * m + b2 * n - (a2 * m + b2 * n) div (a1 * m + b1 *

n) * (a1 * m + b1 * n) >= 0

<S> New C3: (a2 - (a2 * m + b2 * n) div (a1 * m + b1 * n) * a1) * m

+ (b2 - (a2 * m + b2 * n) div (a1 * m + b1 * n) * b1) * n =

a2 * m + b2 * n - (a2 * m + b2 * n) div (a1 * m + b1 * n) *

(a1 * m + b1 * n)

<S> New C5: gcd(a1 * m + b1 * n, a2 * m + b2 * n - (a2 * m + b2 * n)

div (a1 * m + b1 * n) * (a1 * m + b1 * n)) = gcd(m, n)

*** Proved C3: (a2 - (a2 * m + b2 * n) div (a1 * m + b1 * n) * a1) *

m + (b2 - (a2 * m + b2 * n) div (a1 * m + b1 * n) * b1) * n

= a2 * m + b2 * n - (a2 * m + b2 * n) div (a1 * m + b1 * n)

* (a1 * m + b1 * n)

via its standard form, which is:

Std.Fm C3: true

@@@@@@@@@@ VC: procedure_extgcd_3. @@@@@@@@@@

%%% Simplified C2 on reading formula in, to give:

%%% C2: true

>>> Restructured hypothesis H2 into:

>>> H2: n = 0

*** Proved C2: true

--- Eliminated hypothesis H1 (true-hypothesis).

-S- Eliminated hypothesis H2.

This was achieved by replacing all occurrences of n by:

<S> New C1: m = gcd(m, 0)

@@@@@@@@@@ VC: procedure_extgcd_4. @@@@@@@@@@

>>> Restructured hypothesis H6 into:

>>> H6: c - c div d * d = 0

*** Proved C2: d = a1 * m + b1 * n

using hypothesis H3.

-S- Eliminated hypothesis H3.

This was achieved by replacing all occurrences of d by:

a1 * m + b1 * n.

<S> New H2: a1 * m + b1 * n >= 0

<S> New H5: gcd(c, a1 * m + b1 * n) = gcd(m, n)

<S> New H6: c - c div (a1 * m + b1 * n) * (a1 * m + b1 * n) = 0

<S> New C1: a1 * m + b1 * n = gcd(m, n)

-S- Eliminated hypothesis H4.

This was achieved by replacing all occurrences of c by:

a2 * m + b2 * n.

<S> New H1: a2 * m + b2 * n > 0

<S> New H5: gcd(a2 * m + b2 * n, a1 * m + b1 * n) = gcd(m, n)

<S> New H6: a2 * m + b2 * n - (a2 * m + b2 * n) div (a1 * m + b1 *

n) * (a1 * m + b1 * n) = 0

Fig.2(c): EXTGCD.slg simplification log

5 Command-line switches

It is possible to control various aspects of the Simplifier’s behaviour, by including one or more qualifiers on the command-line after the filename.

The general syntax of the SPADE Automatic Simplifier’s command-line is:

command_line = { qualifier_part } filename

qualifier_part = simple_qualifier | log_qualifier |

choices_qualifier | limit_qualifier

simple_qualifier = “-help” | “-version” | “-nolog” |

“-nowrap” | “-verbose” | “-nouserrules” |

“-plain” | “-typecheck” | “-norenum”

log_qualifier = “-log=” filename

choices_qualifier = choices_name [ “=” chosen_units ]

choices_name = “-nosimplification” |

“-nostandardisation” |

“-norule_substitution” |

“-nocontradiction_hunt” |

“-nosubstitution_elimination” |

“-noexpression_reduction”

chosen_units = “(” range { “,” range } “)”

range = integer [ “-” integer ]

limit_qualifier = limit_name “=” integer

limit_name = “-complexity_limit” | “-depth_limit” |

“-inference_limit”

In the above, we do not specify filename or integer further: filename should be a valid filename (possibly with extension, when appearing after the “-log=” qualifier), and integer a decimal integer. Some simplifications of the full syntax may be employed: qualifier names may be abbreviated by omission of trailing letters, provided that the remaining letters specify the qualifier uniquely (e.g. “-nosi” for “-nosimplification”, but not “-nos” as the latter is not unique), and the “(“, “)” parentheses around a list of ranges may be omitted if there is only one range (e.g. “1-2” may appear in place of “(1-2)”, but the parentheses in “(1-2,4)” are compulsory). The compulsory filename which must appear on the command-line (before the qualifiers, if any) should be used to specify the file to be read; the .vcg extension should be omitted. If a device and/or directory is specified, both the .vcg and .fdl file must reside there, and the user must have write access to the directory (as well as to the current working directory), as the output files created by the Simplifier will be written to the same place.

On the command-line, no qualifier may appear more than once; in addition, “-nolog” and “-log=” are mutually exclusive. We consider the consequences of each qualifier in more detail in the following sections.

5.1 Simple qualifiers

The “-help” qualifier instructs the Simplifier to summarise its command-line qualifiers on the screen and exit.

The “-version” qualifier instructs the Simplifier to report its version details on the screen and exit.

The “-nolog” qualifier may be used to indicate that the Simplifier should not generate a .slg log file. The default is that such a file is generated, with the same filename as the input .vcg and .fdl files, but with extension .slg.

The “-nowrap” qualifier suppresses use of the wrap utility (use to line wrap output files). The wrap utility cannot cope with lines exceeding 32767 characters so this switch provides a workaround where the Simplifier generates lines that exceed this length.

The “-verbose” switch causes the listing of simplification actions on the screen. Each is preceded by the time-of-day expressed in hours, minutes and seconds unless the “-plain” switch is also active.

The “-nouserrules” switch suppresses the reading and and use of user-defined proof rules, which is otherwise enabled by default. (Refer to section 7 for more details on the definition and use of user-defined proof rule files.)

The “-plain” switch suppresses the reporting of Date and Time stamps in the Simplifier’s Log file and screen output. This should be used in conjunction with the Examiner’s “-plain_output” option [1] and the POGS tool’s “-i” option [2].

The “-typecheck” qualifier instructs the Simplifier to read in and type-check its input files (e.g. the .vcg, .fdl, and .rls files) only. No Simplification is performed and no output files are generated. This option overrides all other simple qualifiers, and is useful to check the legality of a set of VCs quickly prior to starting a (possibly time-consuming) full simplification run.

The “-norenum” qualifier instructs the Simplifier not to renumber identifiers for hypothesis and conclusions in the output siv file. This provides better traceability of hypothesises and conclusions from siv to the vcg files.

5.2 The log qualifier

The “-log=” qualifier may be used to specify an alternative filename for the log file generated by the Simplifier. If an extension is present on the filename specified, this too is used; otherwise the default extension .slg is appended to the filename specified after this qualifier.

5.3 Choices qualifiers

Choices qualifiers may be used to turn off certain types of Simplifier action for some or all of the VCs in the input file. If the qualifier name is used without a following “=” and chosen_units part, the selected simplification strategy is disabled for all of the VCs in the input file; if some chosen_units are specified, the selected strategy is disabled only for the units in this list. The unit numbers used in such a list should correspond to the numbering used for VCs, counting down from the top and numbering the first entry one.

The six types of strategy which may be disabled are rule substitution, simplification, standardisation, contradiction_hunt, substitution_elimination, and expression_reduction. Referring back to the Simplifier algorithm specified in section 3, we see that disabling rule substitution affects steps 5 and 6 (see sections 3.6 and 3.7 above), disabling simplification affects step 2 (section 3.3) directly and may indirectly affect subsequent steps as a result. Disabling standardisation affects steps 7 (section 3.8), 8 (section 3.9) and 9 (section 3.10) directly, and step 4 indirectly. Disabling the contradiction_hunt affects step 8 (section 3.9) directly and step 9 indirectly. Disabling substitution_elimination affects step 9 (section 3.10, substep (8)) directly and repetitions of step 4 indirectly. Finally, disabling expression_reduction affects step 10 (section 3.10) directly. Disabling one or more strategies for one or more units will result in a faster simplification, but the simplification may in consequence be less effective.

5.4 Limit qualifiers

The three limit qualifiers may be used to alter the numeric upper limit for expression complexity, depth of join search and number of join inferences performed.

The complexity limit determines how “large” an expression the Simplifier will attempt to standardise (when standardisation is enabled — the default). By the size of an expression, we basically mean the number of nodes in the expression tree, e.g. n+1 has complexity 3, while 1*(n+1) has complexity 5. The default complexity limit is 20; if an alternative value is specified in the command-line, it must be an integer in the range 10..200 inclusive.

Section 3.9 (substep 4) above discusses the use of the depth and inference limits in the hypothesis-joining stage of the contradiction hunt. The depth limit’s default value is 5; if an alternative value is specified on the command-line, it must be an integer in the range 1..10 inclusive. The inference limit’s default value is 40; if an alternative value is specified on the command-line, it must be an integer in the range 10..400 inclusive.

6 Log file entries

Each entry in a log file generated by the SPADE Automatic Simplifier is preceded by a three-character symbol which indicates the nature of the simplification action performed. Furthermore, each entry is recorded under a heading which indicates a user rule file summary section or the VC to which the entry is relevant. The hypothesis/conclusion numbers (or path traversal condition numbers) used in an entry are those of the input .vcg file, rather than of the output .siv file, though if restructuring occurs the numbering may change; the numbering is then that of the input .vcg file, but as modified by preceding log entries which record these restructuring actions.

The different symbolic prefixes which may appear in a log file are:

RRS	Header: user defined rules read (only if rule files are present)
&&&	User rule file read in (but not necessarily used)
STX	Header: user defined rules syntax error (only if errors present)
!!!	User defined rule containing at least one syntax error
SEM	Header: warns that user rule semantics are not checked
@@@	Header: indicates start of a new VC
%%%	simplified (with expression simplifier)
>>>	restructured (e.g. by moving negation inwards)
***	proved (one or more conclusions, or the whole VC)
###	contradiction established
---	hypothesis (or traversal condition) eliminated
+++	hypothesis (or traversal condition) added
-S-	substitution performed (eliminating a hypothesis)
<S>	new hypothesis/conclusion as a result of substitution
VCN	Header: summary of user defined rules used by VC n
FIL	At least one user defined rule has been used from this rule file
RUL	This rule from preceding FIL entry has been used at least once
CON	Lists the conclusions proved using the preceding RUL entry
HYP	Lists the hypotheses promoted using the preceding RUL entry
OVR	Header: summary of overall user defined rule use
VCS	Lists the VCs which have used the preceding RUL entry

Note. Where proof-framing has been used to discharge a conclusion, the corresponding log file entries will be indented to reflect any nested subgoaling that occurred during the reasoning, to help make the log file more comprehensible.

The messages related to user defined rule files will only be present if there are rule files read by the simplifier and additionally the user rule summary sections will be present if a user defined rule is used in a proof. Examples of the messages that may occur in a log file are given in section 3.12.

We consider examples of the different messages related to the simplification of a VC which may appear in a log file below.

6.1 Simplification entries

Both hypotheses and conclusions may be rewritten into a simplified form by the expression simplifier during the reading of the .vcg file or subsequently. We may therefore see entries such as:

%%% Simplified H1 on reading formula in, to give:

%%% H1: n = 0

%%% Simplified C3 on reading formula in, to give:

%%% C3: true

%%% Hypotheses H2 & H5 together imply that c = 0.

H2 & H5 have therefore been deleted and a new H2 added

to this effect.

%%% Simplified H2 further, to give:

%%% H2: y = x + 1

%%% Simplified C1 further, to give:

%%% C1: n = 0 -> p(n)

for VCs.

Two hypotheses (or traversal conditions) may sometimes be collapsed into one equality as the above message samples illustrate. This occurs if, for instance, we have hypotheses that a>=b and a<=b, which can be combined to give a=b instead.

6.2 Restructuring entries

Restructuring occurs as a result of global logical simplifications, as outlined in section 3.4 above. The following messages may be seen when simplifying VC files:

>>> Hypothesis H4 has now been split into two, giving:

>>> H4: a = b + c

>>> H7: p(a)

>>> Restructured hypothesis H1 into:

>>> H1: true

>>> Conclusion C1 has now been split into two, giving:

>>> C1: n * n >= 0

>>> C2: n * n < r + 1

>>> Using “A->B, A |- B” on H6 given that “A” is obvious,

we simplify this to:

>>> H6: p(x)

>>> Using “A->B, A |- B” on H6 given H3 & H5, we simplify

the former to:

>>> H6: p(x)

>>> Attempting to prove quantified formula C2 by “unwrapping” it.

>>> Conclusion C4 is an implication formula [P->Q].

Attempting to prove this by proving Q while adding P to the

hypotheses.

>>> Attempting to prove C3 by cases, depending on whether

(1) n = int_i_1, or

(2) n <> int_i_1,

given the need to simplify update(A, [I], X) accesses in C3.

The first message (split) occurs when a conjunction hypothesis (which may have become a conjunction as a result of other simplifications and/or restructuring) is split into two parts. The second occurs when, as a result of moving negation inward and simplifying, the expression is restructured to a new form. The last two forms apply when a hypothesis (or less likely, a traversal condition) of the form A->B can be converted into B, as the inference engine is capable of establishing that A holds. The first form of this message occurs when A can be inferred without reference to any other hypothesis; the second form is used when one or more other hypotheses are used in discharging the proof of A. The last three forms of message for VC files indicate that a proof-framing attempt is underway.

6.3 Proof Entries

If the Simplifier manages to discharge the proof of any (or all) of the conclusions of the current VC, entries such as:

*** Proved C5: d > d - 1

via its standard form, which is:

Std.Fm C5: true

*** Proved C5: d > 0

using hypotheses H2, H3 & H6.

*** Proved C2: for_all(i:integer, element(a, [i]) <= 10)

by unwrapping a universally-quantified formula.

*** Proved C3: x >= 1 -> x >= 0

by implication.

*** Proved C4: element(update(a, [i], x), [j]) >= 1

by cases on index values, given the update(A, [I], X)

subexpressions.

*** Proved subgoal C1: d > d - 1

via its standard form, which is:

Std.Fm C1: true

*** Proved subgoal C1: d > 0

using hypotheses H2, H3 & H6.

*** PROVED VC.

appear in the log, to record which were proved and how.

6.4 Contradiction entries

For VCs, we may see a message of the form:

### Established a contradiction [HOW].

if a contradiction is established. If more information is available on the hypotheses (or traversal conditions) used, this may appear as:

### Established a contradiction [HOW] using hypothesis H4.

### Established a contradiction [HOW] among the following

hypotheses:

H1, H3 & H8

The “HOW” part will be instantiated to a particular method, which will be one of the following:

false-hypothesis

P-and-not-P

empty-range

contradictory-combination

contradiction-through-substitutions

which give some indication of how the contradiction was arrived at.

6.5 Hypothesis elimination entries

For VCs, we may see the following hypothesis/conclusion elimination messages:

--- Attempted addition of new hypothesis:

a = b - 1

eliminated: this already exists (as H2).

--- Eliminated hypothesis H4 (HOW).

--- Eliminated hypothesis H4 (HOW, given H1).

--- Eliminated hypothesis H6, which only specifies a value

for x1.

This is not referred to anywhere else in the VC.

--- Eliminated conclusion C4, which is a duplicate of C2.

Where there is a “HOW” part to indicate the method of elimination, the explanatory text will be one of the following forms:

true-hypothesis

true-disjunction

duplicate of Hn

implied by Hn

equivalent to Hn

P-or-not-P disjunction

redundant.

6.6 Hypothesis addition entries

The Simplifier may be able to spot that the left-hand side of an implication (or either side of an equivalence) hypothesis can be discharged by the inference engine, using the other hypotheses. Where this occurs, one may see a message of the form:

+++ Using “A->B, A |- B” on hypotheses H3 & H5 yields a

new hypothesis:

+++ H9: a * b <= 4

+++ Using “A->B, not B |- not A” on hypotheses H2 & H7

yields a new hypothesis:

+++ H8: r * r = 0

+++ Added new hypotheses (in proving an implication formula).

+++ New H21: 1 <= int_i_1

+++ New H22: int_i_1 <= 20

+++ Case 1 – New H25: n = loop__1__i

+++ New subgoal C1: 0 <= x and x <= 100

6.7 Substitution entries

Where substitution of values for variable identifiers has taken place during simplification, this is recorded by entries of the following form for VC files:

-S- Eliminated hypothesis H10.

This was achieved by replacing all occurrences of x

by:

a * a - 2 * a * b + b * b.

<S> New H6: p(a * a - 2 * a * b + b * b)

<S> New C4: a * a - 2 * a * b + b * b = (a - b) * (a - b)

Thus, the -S- shows the actual substitution that occurred (and the hypothesis which was eliminated, or traversal condition that was employed), and the <S> entries record the effect of the substitution on individual hypotheses and conclusions (or traversal conditions and the action part).

Additionally, a substitution may occur as the result of application of a substitution rule. This is signalled by:

-S- Applied substitution rule const(5).

This was achieved by replacing all occurrences of c

by:

42.

Individual <S> facts will then follow, as above for a substitution resulting from the elimination of a hypothesis.

6.8 Side-condition entries

In applying a user-defined inference or rewrite rule, the log file will record the rule match used, together with each of the side-conditions of the rule match and how these were established. Each such side-condition satisfaction entry is signalled by ‘<<<’, e.g.

*** Proved C3: sum_of_range(a, 1, loop__1__i) +

element(a, [loop__1__i+1]) = sum_of_range(a, 1, loop__1__i+1)

This was achieved by applying the rewrite rule sum_rule(3)

[from rulefile sumarray.rlu] to rewrite this conclusion to:

<S> C3: sum_of_range(a, 1, loop__1__i) + element(a, [loop__1__i +

1]) = sum_of_range(a, 1, loop__1__i) + element(a, [

loop__1__i+1])

This rule could be applied because its side-conditions hold, as

follows:

<<< By simple reasoning, proved: sum_of_range(a, 1, loop__1__i)

+ element(a, [loop__1__i + 1]) = sum_of_range(a, 1,

loop__1__i) + element(a, [loop__1__i + 1])

<<< By simple reasoning, proved: 1 <= 1

<<< From H5, proved: 1 <= loop__1__i

<<< From H14, proved: loop__1__i + 1 <= 100

For each side-condition, the entry records whether it was trivially true, or whether it was deduced from one or more hypotheses.

6.9 Null entries

The only other entry that should be observed from time to time is:

NO SIMPLIFICATION ACTIONS PERFORMED.

This occurs when none of the Simplifier’s strategies succeed in modifying the given VC.

7 User-defined proof rules

7.1 Naming of user-defined proof-rule files

When the Simplifier is applied to a VC file xxx.vcg whose immediately-enclosing directory is named ddd, the Simplifier will attempt to locate and read two files within the same directory as the .vcg file which, if present, are assumed to contain definitions of user-defined proof rules. The first file it will look for is called ddd.rlu, where ddd is the directory-name. (This allows a common set of proof rules to be applied to all of the subprograms within a directory, in a simple manner.) The second file it will look for is called xxx.rlu, where xxx is the name of the .vcg file. Each of these files will be read if it is present, unless the -nouserrules switch (see section 5.1) has been used on the command-line to override this. It is not an error for either, or both, files to be absent: the absence of user-defined proof-rules merely means that such rules will not be read in and made use of.

The extension .rlu has been chosen for such proof-rule files to distinguish them from .rls files, which is the extension used for the Examiner-generated file of proof-rules for each subprogram, and from .rul, which is generally and historically used for proof-rule files constructed for use with the SPADE Proof Checker. Mnemonically, one can think of ‘.rls’ as standing for “RuLes (SPARK)” and ‘.rlu’ for “RuLes (User)” respectively.

7.2 Syntax and semantics of proof rules

The SPADE Automatic Simplifier supports two different types of rule, inference rules and rewrite (or “substitution”) rules. The inference rules can be used to state under what conditions a goal formula can be inferred from (zero or more) existing facts, while the rewrite rules allow a subexpression of the VC to be replaced by an equivalent subexpression in the right circumstances.

Each type of rule has conditions associated with it which must hold if the rule is to be applicable: in the former case, these conditions are the facts to be combined, whereas in the latter case they are facts which must hold to ensure the equivalence is true. For example, the formula (A and B) may be replaced by the formula A if we know that the condition B holds, because if B is true then (A and B) is effectively the same as (A and true), which can be simplified to A. Given this reasoning, it is valid to define (A and B) may_be_replaced_by A if [B] as a proof-rule. But note that, while a rule such as X>=Y may_be_deduced_from [X>Y] is legal as an inference rule, the rewrite rule X>=Y may_be_replaced_by X>Y is not valid: it would allow us to rewrite a hypothesis such as r>=s into r>s, which strengthens the original hypothesis without any justification for doing so.

For either type of rule, some of the conditions may be “meta-logical” in that they refer to type-checking constraints or other externally-evaluable conditions. Before we consider in greater detail the conditions which may be applied, we first turn our attention to the syntax of each type of rule in turn.

Please note that, in the following sections, the metalanguage used is a modification of Backus-Naur form employed in BS 6192: 1982.

7.2.1 Inference rules

Inference rules allow existing facts (i.e. hypotheses, their immediate consequences, trivial truths such as 2+1=3 and other immediate constraints) to be combined to infer new facts, which may then be added to the VC as new hypotheses. The general syntax of an inference rule is:

inference-rule = rulename “:” formula conditional-part.

where

conditional-part = “may_be_deduced_from” list-of- conditions

| “may_be_deduced”

rulename = family-name”(“ specific-rule-number “)”

specific-rule-number = non-negative-integer

formula = well-formed-prolog-expression

list-of-conditions = “[” “]” | “[” condition { “,” condition } “]”

condition = ordinary-condition | immediate-condition

ordinary-condition = well-formed-expression

immediate-condition = “goal(” well-formed-expression “)”

We discuss the list of conditions in section 7.2.3 below. The family-name of a rule should be an identifier, composed only of lowercase letters, the digits 0..9 and underscores, and commencing with a lowercase letter. The family-names selected for user-defined rules should be descriptive but reasonably succinct, for ease of legibility and reference. Furthermore, each rule should be uniquely identified: you should not specify two rules each called my_rule(1), for instance. The Simplifier will complain on-screen about any malformed or repeated rulenames it encounters as it reads in each user-defined proof-rule file, and will discard the corresponding rule, so that such rules will not be available for the Simplifier to use in its proof attempts.

The formula, a ‘well-formed expression’, may contain “Prolog variables” or “wildcards”, which are identifiers that begin with a capital letter. Indeed, this is very much the norm: a rule without Prolog variables should be rare, and only used in practice to carry across relationships which must hold between program constants, e.g. that maxchars=<maxlen, where both are declared as “constants” in the source code and so do not change. (By adding such rules about the relationships between program constants, we can declare properties which we require to hold for the eventual program, regardless of the actual values eventually chosen for these constants.)

(Note that proof-rules use FDL syntax. This means that each well-formed expression within a proof rule must use FDL syntax, rather than that of SPARK. Thus, we use update(A, [I], X) for array update expressions rather than A[I => X], fld_f(R) rather than R.f, etc.)

Returning to the use of Prolog variables in rules: they allow the rule to express a general property, and the rule is used by instantiating its Prolog variables to specific values. For example, the (hypothetical) inference rule

my_rule(1): A >= B may_be_deduced_from [A >= 0, B <= 0].

is essentially universally-quantified over A and B: it says that, for all A and B (of an appropriate numeric type, given the list of conditions associated with the rule), if we know A>=0 and also B<=0, then we can infer that A>=B holds also. (Note that the scope of each such Prolog variable is limited to the rule within which it occurs, so the use of A in one rule does not interfere with the use of A in any other rule.)

Each inference rule is essentially an implication formula. The rule

my_rule(2): Goal may_be_deduced_from [ Fact1, Fact2, Fact3].

is essentially short-hand for the formula

(Fact1 and Fact2 and Fact3) -> Goal

In order for the Simplifier to be able to make use of the rule, it must find an instance of the rule by pattern-matching it against the current VC (for inference rules, this essentially means against the undischarged conclusions of the VC) in such a way that each of the capital-letter Prolog variables in the rule become ‘instantiated’ to particular expressions (involving literals, identifiers and expressions present in the VC). For example, given the VC

H1: n >= 1 .

C1: f(n) >= 0 .

and the proof rule

f_property(1): f(X) >= 0 may_be_deduced_from [X >= 0].

an instance of this rule can be found by letting the wildcard X take the “value” n; in doing so, the instance of the rule is

f_property(1): f(n) >= 0 may_be_deduced_from [n >= 0].

which can be used to infer C1 directly, provided the list of conditions (in this case, consisting of the single condition n>=0) can be established (which it can from H1 here, since if n>=1, then n>=0 holds, too.)

Of course, there are other instances of the rule f_property(1), too: e.g. we could choose n+1 for X, or n*n+1, or 42, or any value which gives a legal type-check to the rule. (This latter caveat means that we cannot legally choose true, however, as an instance for X.) But the only really useful match, in the case of the above VC, is to choose n for X, by ‘pattern-matching’ the rule with the existing VC’s conclusions; we’ll look at pattern-matching in more detail in section 7.3 below.

7.2.2 Rewrite rules

Rewrite rules allow one subexpression of a VC (either a conclusion, or a hypothesis) to be replaced by another, equivalent, expression. For compatibility with the SPADE Proof Checker, there are two types of rewrite rule: one-way and two-way rules. Their general syntax is described below, with the definition of the rulename and condition-list parts as for inference rules, described in the previous section.

rewrite-rule = rulename “:” one-way-rule “.” | rulename “:” two-way-rule “.”

one-way-rule = expression “may_be_replaced_by” expression [ “if” list-of-conditions ]

two-way-rule = expression “&” expression “are_interchangeable”

[ “if” list-of-conditions ]

where

expression = well-formed-expression

The same remarks as we made about the choice of rule-names for inference rules in the preceding section apply to rewrite rules, too.

Note that the distinction between one-way and two-way rules is only made very weakly when the Simplifier attempts to apply these rules, however. In pattern-matching against a one-way rule, the Simplifier will first try the ‘correct’ orientation, but it will also try applying the rule the other way round, too.

As with the inference rules, most substitution rules contain Prolog variables so that they express a general property, specific instantiations of which are used in applying such rules. To be used, a substitution rule also requires that both expressions (the expression to be replaced and the expression by which it is to be replaced) be fully instantiated, in line with a similar constraint on the use of inference rules. The list of conditions, both for substitution rules and for inference rules, are discussed in the next section.

Semantically, a rewrite rule of the form

my_rule(3): A may_be_replaced_by B if [ Fact1, Fact2, Fact3].

is also expressing an implication formula, but one whose right-hand side is an equality, thus:

(Fact1 and Fact2 and Fact3) -> A=B

The rule allows us to replace a subexpression of the form A (whether in a conclusion or a hypothesis) by the expression B, provided we can establish that all of the conditions in the list of side-conditions (in this instance, Fact1, Fact2 and Fact3) hold.

7.2.3 Condition lists

Each inference rule or rewrite rule may have a list of side-conditions associated with it. In order for the rule to be legally applied, the Simplifier must find an instance of the rule by pattern-matching (see next section) in which each of the side-conditions can be satisfied (see section 7.4 for details of how this is achieved).

Within the conditions list, two sorts of condition are permitted: logical conditions, and meta-logical conditions.

Logical conditions are well-formed expressions which, when instantiated, must type-check as boolean and can be solved in the normal way by the Simplifier’s built-in inference engine. For example, the rule instance of f_property(1) in section above (with n for X) gave rise to a single condition n>=0, which we can reasonably hope that the Simplifier’s inference engine will establish given H1 of the VC shown.

Meta-logical conditions are ones which are not strictly part of the FDL language of expressions, but which invoke some ‘evaluation’ within the Simplifier to determine whether the corresponding constraint holds. Meta-logical conditions are indicated by taking the form goal(X), where X is the meta-logical condition to be evaluated. There are six legal meta-logical conditions that may appear in a list of side-conditions, as follows.

· goal(integer(N)). For this meta-condition to hold, N must be instantiated to an integer literal by the time the meta-condition is evaluated. Thus, goal(integer(42)) would succeed, while goal(integer(true)), goal(integer(2+3)) and goal(integer(11/3)) will all fail (as will goal(integer(V)) if V is still a wildcard by the time the meta-condition is evaluated: we’ll return to this in more detail in sections 7.3 and 7.4 below).

· goal(intexp(E)). This is similar to goal(integer(E)), but slightly more liberal, in that it also allows general expressions which are integer by construction, provided each leaf of the expression tree for E is an integer literal. Thus, both goal(intexp(42)) and goal(intexp(2+3)) will succeed, but goal(intexp(true)) and goal(intexp(11/3)) will still fail, in the latter case because “/” is the real division operator. (Note that this means that goal(intexp(12/3)) will also fail, though goal((simplify(12/3,N), intexp(N))) will succeed, because the simplified value of 12/3 that this gives to N is 4.)

· goal(checktype(E,T)). For this to succeed, E must be instantiated to an expression which contains no uninstantiated wildcards and which type-checks correctly by the time the condition is evaluated (so x+1=y is acceptable if x and y are of type integer, for instance, but not if one or both is of type boolean, say, or of an array or record type). In addition, T must either be a wildcard at the time the meta-condition is evaluated (in which case it becomes instantiated to the corresponding type, e.g. goal(checktype(1+2,T)) succeeds, and sets T to be integer), or it must be an identifier that signifies a type-mark (in which case the meta-condition will succeed only if the corresponding expression E can indeed be ascertained to be of type T).

· goal(simplify(E,V)). For this to succeed, E must be instantiated to an expression which contains no uninstantiated wildcards by the time the condition is evaluated. In general, V should still be a wildcard at the point of evaluation of the condition; if it is, and E is a well-formed expression that can be simplified, then V will be its simplified form, which may be unchanged (e.g. goal(simplify(1+2*3,V)) succeeds and sets V to 7, goal(simplify(x+y,V)) succeeds and sets V to x+y). Alternatively, V could be fully-instantiated by this point, in which case goal(simplify(E,V)) will only succeed if goal((simplify(E,W)) succeeds (for wildcard W) and V happens to have the same value as W.

· goal((X,Y)). This is shorthand for the conjunction of two meta-logical conditions (note the additional inner parentheses, which are mandatory). Within a condition list, [... goal((X,Y)), ...] will succeed precisely when [... goal(X), goal(Y), ...] succeeds. (Indeed, the latter is to be preferred.)

· goal((X;Y)). This is shorthand for the disjunction of two meta-logical conditions (note the additional inner parentheses, which are mandatory). Within a condition list, goal((X;Y)) will succeed when either goal(X) or goal(Y) (or both) would succeed, and will fail if both fail. (An alternative means of achieving the same effect is to have two separate proof rules, in one of which goal(X) occurs, in the other of which goal(Y) occurs, but which are identical apart from this single difference. This separation into two rules is to be preferred.)

7.2.4 Comments

Comments are supported within user-defined rule files and the syntax follows Prolog /*…*/ rather than the Ada – style:

/* This is my first user-defined proof rule. */

my_rule(3): A may_be_replaced_by B if [ Fact1, Fact2, Fact3].

7.3 Pattern-matching against proof rules

7.3.1 Inference rules

For an inference rule of the form

rulename(1): Goal may_be_deduced_from Conditions.

the Simplifier will attempt to find a means of instantiating all of the wildcards in Goal such that it becomes an exact match for an existing undischarged conclusion. In doing this, all of the wildcards in Goal must become instantiated to non-wildcards, and as a side-effect of doing so some – possibly all – of the wildcards in the list Conditions will also become instantiated, too.

For example, given the conclusion

C1: f(a, b * b) >= c + 1 .

and the rule

f_property(2): f(X,Y) >= Z may_be_deduced_from

[ X >= W, Y >= W, W>=Z].

if we pattern-match f(X,Y) >= Z against C1, we must choose to instantiate X to a, Y to b*b and Z to c+1. This gives us the condition-list [a>=W, b*b>=W, W>=c+1], in which all three conditions are only partially instantiated (as the wildcard W still occurs in all three conditions).

Note that if C1 was instead

C1: f(a, b * b) > c + 1 .

or even

C1: not (f(a, b * b) < c + 1) .

the pattern-matching would fail: the main operator of the goal formula in the rule (the “>=” operator) must be the same as that of the conclusion if we are to be able to pattern-match the two together. (N.B. The latter form is,however, unlikely to persist in conclusion formulae by the time the user-defined rules are applied, as such a form is likely to already have been simplified in earlier phases of simplification.)

7.3.2 Rewrite rules

For a rewrite rule of the form

rulename(2): Old may_be_replaced_by New if Conditions.

The pattern-matching against a conclusion of the VC proceeds as follows.

If Old can be pattern-matched to the toplevel conclusion formula, this is a match. Otherwise, we look at its immediate subexpressions, and try pattern-matching against these in turn (in left-to-right order), and to the subexpressions of these expressions, and so on. Finding a match will instantiate the wildcards in Old, and will generally instantiate some (or all) of those in New and in the Conditions list.

For example, given the conclusion

C1: f(a, f(b, c)) = f(f(a, b), c) .

and the rule

f_property(3): f(X,Y) may_be_replaced_by f(Y,X)+1 if

[X > Y].

the following pattern-matches of f_property(3) against C1 are possible:

1 Match against the left-hand side of C1 by matching X to a, Y to f(b,c), to allow f(a,f(b,c)) to be rewritten to f(f(b,c),a)+1 if [a>f(b,c)];

2 Match against the inner application of f on the left-hand side of C1, by matching X to b, Y to c, to allow f(b,c) to be rewritten to f(c,b)+1 if [b>c];

3 Match against the right-hand side of C1 by matching X to f(a,b), Y to C, to allow f(f(a,b),c) to be rewritten to f(c,f(a,b))+1 if [f(a,b)>c];

4 Match against the inner application of f on the right-hand side of C1 by matching X to a, Y to b, to allow f(a,b) to be rewritten to f(b,a)+1 if [a>b].

In each of these pattern matches, all of the wildcards in the rule become fully instantiated as a side-effect of finding the means of matching the rule-pattern to the subexpression in the conclusion formula.

Rewrite rules can also be pattern-matched against hypotheses and subexpressions of hypotheses, generating new facts that can be added to the hypotheses (provided the conditions of the rule-match can be discharged). The same process is applied in this case also.

7.4 Satisfaction of a proof-rules list of side-conditions

Having found an inference-rule pattern-match, the list of conditions will consist of zero or more fully-instantiated conditions, and zero or more partially-instantiated conditions.

The Simplifier proceeds to try to satisfy such a condition list by splitting in into these two sublists (fully instantiated and partially instantiated), while retaining the same left-to-right order within each of these sublists.

The next step is to try to satisfy each of the fully-instantiated conditions. For each of these in turn, the Simplifier’s inference engine is invoked to attempt to discharge the condition. If the proof succeeds, the number of unsatisfied conditions reduces by one. Otherwise, the Simplifier tries to use the inference engine to establish the negation of the condition it hasn’t been able to prove: if this succeeds, the current instantiation of the rule-match is abandoned, since at least one of the conditions is false, so the rule can never be constructively applied. This proceeds until either all the fully-instantiated conditions have been proved, or at least one has been shown to be false and the match abandoned.

(For any meta-conditions encountered in this process, they are evaluated and either succeed, allowing the rule-match exploration to continue, or fail, and cause the rule-match to be abandoned.)

In the case where all the fully-instantiated conditions hold, the next step is to try to find instantiations of the remaining wildcards in the rule which are useful, in that they make the remaining unsatisfied conditions satisfiable. For example, in attempting to apply rule f_property(2) in section 7.3.1 above, we ended up with a partially-instantiated condition list [a>=W, b*b>=W, W>=c+1]. The Simplifier tries various means of satisfying these, again searching in left-to-right order. For example, choosing a for W satisfies condition 1 trivially, and makes the remaining conditions [b*b>=a, a>=c+1] fully-instantiated: we can then try these. Another means of satisfying this first condition is to try a form of pattern-matching of the condition against the existing hypotheses, to see if we have a hypothesis a>=Something, since that Something is then a candidate for W. This proceeds until all straightforward potential solutions of the first condition have been explored, then candidate solutions for the second are explored, and so on until the candidate solution generator has exhausted all of its options.

At each stage, when one or more partially-instantiated conditions is ‘solved’ and made fully-instantiated, the conditions list is repartitioned, gradually increasing the fully-instantiated list and reducing the partially-instantiated list, until the latter is empty (which it must be for the rule match to be permissible).

The same process (of splitting, inferring and solving) is used for satisfying the conditions list when applying rewrite rules. Provided the conditions list can be satisfied, the rewrite rule can be applied as appropriate to the corresponding conclusion or hypothesis.

7.5 Examples of user-defined proof rules

7.5.1 Greatest common divisor

The greatest common divisor function, gcd(X,Y) has a number of properties that can be expressed via proof rules, including:

gcd_rule(1): gcd(X, Y) may_be_replaced_by gcd(Y, X)

if [X >= 0, Y >= 0].

gcd_rule(2): gcd(Y, X - X div Y * Y) may_be_replaced_by gcd(X, Y)

if [X >= 0, Y > 0].

gcd_rule(3): gcd(X, 0) may_be_replaced_by X

if [X > 0].

Note that these rules are ‘non-terminating’, in that they can be repeatedly applied. For example, rule gcd_rule(1) allows gcd(a,b) to be rewritten to gcd(b,a), which can then be rewritten to gcd(a,b), etc. The Simplifier currently only applies the set of rules to a small depth, so that such non-termination cannot cause a problem.

The above set of three rules is nevertheless sufficient to discharge the following two VCs, which would otherwise remain undischarged after simplification:

procedure_calculate_gcd_4.

H1: d > 0 .

H2: gcd(m, n) = gcd(c, d) .

H3: m >= 1 .

H4: m <= 2147483647 .

H5: n >= 1 .

H6: n <= 2147483647 .

H7: c >= 0 .

H8: c <= 2147483647 .

H9: d <= 2147483647 .

H10: c div d >= 0 .

H11: c div d <= 2147483647 .

H12: 0 < c - c div d * d .

H13: c - c div d * d <= 2147483647 .

C1: gcd(m, n) = gcd(d, c - c div d * d) .

and

procedure_calculate_gcd_12.

H1: d > 0 .

H2: gcd(m, n) = gcd(c, d) .

H3: m >= 1 .

H4: m <= 2147483647 .

H5: n >= 1 .

H6: n <= 2147483647 .

H7: c >= 0 .

H8: c <= 2147483647 .

H9: d <= 2147483647 .

H10: c div d >= 0 .

H11: c div d <= 2147483647 .

H12: c div d * d <= 2147483647 .

H13: c - c div d * d = 0 .

C1: d = gcd(m, n) .

7.5.2 Sum of the elements of an array

The function sum_of_array(A) is intended to represent the value of the sum of all of the elements of an array A. We can define it in terms of another proof function, thus:

sum_rule(1): sum_of(A) may_be_replaced_by

sum_of_range(A, indextype__first, indextype__last).

sum_rule(2): sum_of_range(A, L, L) may_be_replaced_by

element(A, [L]) if

[ indextype__first <= L, L <= indextype__last ].

sum_rule(3): sum_of_range(A, L, U+1) may_be_replaced_by

sum_of_range(A, L, U) + element(A, [U+1]) if

[ indextype__first <= L, L <= U,

U+1 <= indextype__last ].

The first rule defines the overall proof function in terms of a sum_of_range function, which defines the sum over a given index range (whose lower and upper bounds are the second and third arguments of this function respectively). The second and third rules provide a recursive definition (base case for the unit range, then recursion case which extends the range) of this proof function. These three rules are sufficient to discharge the following three partial correctness VCs for an implementation of array sum (with index range 1..100), which would otherwise remain undischarged by the Simplifier:

procedure_sumarray_4.

H1: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 100 ->

0 <= element(a, [i___1]) and element(a, [i___1]) <= 1000) .

H2: element(a, [1]) >= 0 .

H3: element(a, [1]) <= 100000 .

C1: element(a, [1]) = sum_of_range(a, 1, 1) .

procedure_sumarray_5.

H1: 0 <= sum_of_range(a, 1, loop__1__i) .

H2: sum_of_range(a, 1, loop__1__i) <= loop__1__i * 1000 .

H3: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 100 ->

0 <= element(a, [i___1]) and element(a, [i___1]) <= 1000) .

H4: loop__1__i >= 1 .

H5: loop__1__i < 100 .

H6: sum_of_range(a, 1, loop__1__i) + element(a, [loop__1__i + 1])

>= 0 .

H7: sum_of_range(a, 1, loop__1__i) + element(a, [loop__1__i + 1])

<= 100000 .

C1: sum_of_range(a, 1, loop__1__i) + element(a, [loop__1__i + 1]) =

sum_of_range(a, 1, loop__1__i + 1) .

and

procedure_sumarray_6.

H1: 0 <= sum_of_range(a, 1, 100) .

H2: sum_of_range(a, 1, 100) <= 100000 .

H3: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 100 ->

0 <= element(a, [i___1]) and element(a, [i___1]) <= 1000) .

C1: sum_of_range(a, 1, 100) = sum_of(a) .

7.6 Construction and soundness of user-defined proof rules

While the construction of user-defined proof rules allows the user to directly extend the power of the Simplifier in a simple manner, it also brings risk that the user will add rules that are not sound, and use these unsound rules to discharge VCs that are not provable. Your attention is drawn to this very real possibility: you should be aware that the Simplifier has no means of checking that the rules you write are sound.

Ideally, in constructing your own user-defined proof rules, you should restrict yourself to rules that provide definitions and simple properties of proof functions that you have used to annotate your code for proof. Examples would include the gcd and sum_of_array functions that we considered in the preceding section: these illustrate what can be done, and how to use side-conditions to enforce the necessary constraints that make these definitions and properties meaningful.

Typically, such proof function rules will consist either of definitional rules, allowing the general form of the proof function – f(A,B,C,...), for wildcards A,B, C, ... – to be replaced by an expression defined in terms of these arguments, or a number of specific cases defining the function, each distinguished via the side-conditions imposed by the rules. You must still establish the soundness of these rules, if any proofs constructed with them by the Simplifier are themselves to be valid.

Where more general purpose rules are to be constructed and used, ensure that you can construct a formal proof of the rules. For example, we might define a rule

arith(2): X - Y <= N may_be_deduced_from

[goal(integer(N)),

N > 0,

-N <= X,

X <= N,

-N <= Y,

Y <= N,

(X >= 0 and Y >= 0) or (X <= 0 and Y <= 0)].

which is useful in proving a particular VC. This rule is in fact valid, but to establish this requires a proof to be constructed – ideally, with the Proof Checker (that the implication formula to which this rule corresponds is true), or with some other tool or manually (though in the latter case, the manual proof needs to be rigorous if we are to be able to rely on it).

7.6.1 Free variables within condition lists

In constructing proof rules, try to avoid wildcard goal formulae or general wildcard expressions within proof rules. For example,

rule(1): X may_be_deduced_from

[Y -> X, Y]

is a valid rule, but it will match against anything: X can be instantiated to any formula, which means it will match with every unproved conclusion in turn. Similarly,

rule(1): X may_be_replaced_by Y if [X=Y]

will match against every subexpression of every conclusion and hypothesis, generating a vast number of potential pattern-matches to explore. Much better to avoid such generalisations (which are accommodated by the Simplifier’s built-in strategies in any case, for the above two rules) and construct specific rules about specific formula patterns and specific subexpression patterns, providing at least one function/operator within the formula or expression – more, if this is reasonable.

If the use of a general wildcard expression is unavoidable or appropriate then it is desirable that the side conditions involving free variables in the condition list are suitably constrained to minimise the potential search space. If there is more than one side condition involving a free variable place the more constrained before the less constrained in the condition list. For example:

rule(2): B - 1 >= C + 1 may_be_deduced_from

[A + B = 2*C + 1,

A < C,

goal(checktype(A, integer)),

goal(checktype(B, integer)),

goal(checktype(C, integer)) ].

In rule(2) A is a free variable in the condition list but the first side condition places the most stringent constraints on the variable A than any of the other side conditions.

7.7 Logging the use of user-defined proof rules

When user-defined proof rules are used in constructing the proof of one or more conclusions of a VC, this is recorded within the .slg log file: see section 6.8 for details on the form of these log file entries.

In addition, if no conclusions remain unproved after application of the user-defined proof rules, this is indicated within the .siv file. The VC will still be “true”, but it will be followed by the comment

/* proved using user-defined proof rules. */

as an additional record of the fact that user-defined proof rules were used.

Document Control and References

Altran Praxis Limited, 20 Manvers Street, Bath BA1 1PX, UK.

File under

SVN: trunk/userdocs/Simp_UM.doc. (Was formerly filed in S.P0468.73.27)

Changes history

Issue 1.0: (1st September 1997): After review by Ian O’Neill.

Issue 1.1: (16th December 1997): Reissued with minor formatting changes.

Issue 1.2: (5th July 2000): Minor formatting changes as part of Release 5.0 updates

Issue 2.0: (10th July 2000): After review

Issue 2.1: (16th October 2001): First draft for Simplifier release 2.0, for toolset release 6.0.

Issue 2.2: (26th October 2001): Added documentation of new SPARKSimp tool.

Issue 3.0 (4th November 2001): Definitive issue following review S.P0468.79.74.

Issue 4.0 (25th March 2003): Updated to new template format

Issue 5.0 (30th May 2003): Changes to new template, final format

Issue 5.1 (5th June 2003): Adds documentation of /norule_substitution switch.

Issue 5.2 (10th July 2003): Adds documentation of sparksimp “echo” switch.

Issue 5.3 (2nd October 2003): Adds documentation of sparksimp “processes” switch.

Issue 5.4 (12th March 2004): Revision to address Simplifier “proof-framing” enhancement

Issue 5.5 (23rd March 2004): Minor corrections following formal review.

Issue 5.6 (25th November 2004): Change company trading name and updates for SPARKSimp 2.5.

Issue 5.7 (5th January 2005): Definitive issue following review S.P0468.79.88.

Issue 5.8 (12th April 2005): Draft issue, added documentation of sparksimp echoing errors to screen.

Issue 5.9 (12th December 2005): Draft issue, added documentation of user-defined proof rules and its command-line switch, plus additional small changes resulting from other recent changes to the simplification process.

Issue 5.10 (15th December 2005): Definitive issue, following formal review.

Issue 5.11 (13th January 2006): Definitive issue following reviews S.P0468.79.90 and S.P0468.59.10.

Issue 5.12 (24th February 2006): Document /typecheck switch (CFR 1617).

Issue 5.13 (12th June 2006): Document /noexpression_reduction switch (CFR 1646).

Issue 5.14 (20th June 2006): Document /x=Simpexec switch (CFR 1652).

Issue 5.15 (15th January 2007): Document comment style supported (CFR 1737).

Issue 5.16 (16th May 2007): Additional log file output (CFR 1742).

Issue 5.17 (28th August 2007): Document removal of /memory switch and change of /noecho to default.

Issue 5.18 (14th July 2008): Updates following review S.P0468.79.93

Issue 5.19 (26th August 2008): Preferred switch character is now ‘-‘ on all platforms.

Issue 5.20 (2nd September 2008): Describe help, version and verbose qualifiers.

Issue 5.21 (7th January 2009): Factored out contact details.

Issue 5.23 (20th November 2009): Remove all reference to Path Functions.

Issue 5.24 (3rd February 2010): Rebrand to Altran Praxis Limited

Issue 5.25 (19th February 2010): Subsection 7.6 to create 7.6.1 and include ordering of side conditions

Issue 5.26 (19th February 2010): Rewrote Sect.8: SPARKSimp switches and ZombieScope invocation.

Issue 5.27 (30th March 2010): Removed section on usage profiling.

Issue 5.28 (12th October 2010): Correct references to the Examiner.

Issue 5.29 (1^st November 2010): Removed description for SPARKSimp. A new user manual has been added for this instead.

Issue 5.30 (14th June 2011): Added time-stamps in verbose mode screen output. [K608-018]

Changes forecast

None.

Document references

1 Examiner User Manual

2 POGS User Manual

3 ZombieScope User Manual

[1] Note: The SPARK programming language is not sponsored by or affiliated with SPARC International Inc. and is not based on SPARC™ architecture.

[2] In fact, these substitutions do not really occur once per VC, but are instead performed once on start-up, prior to simplifying any VCs, as we shall see in more detail in the next section.


		SPARK Simplifier User Manual



		SIMPLIFIER/UM Issue: 5.30 Status: Definitive 14th June 2011 DOCTYPE:Praxis title:varchar=title reference:varchar=reference status:varchar=status issue:varchar=issue date:varchar=date projectname:varchar=DocumentSet Issue 5.29, Definitive, 1st November 2010 000_000 User Manual
		Originator
		SPARK Team
		Approver
		SPARK Team Line Manager