SPADE Proof Checker

Rules Manual

 

 

 

 

 

 

 

 

 

 

 

SPDRM

Issue: 6.2

Status: Definitive

12th October 2010

 

DOCTYPE:Praxis title:varchar=title reference:varchar=reference status:varchar=status issue:varchar=issue date:varchar=date projectname:varchar=DocumentSet

Issue 6.0, Definitive, 17th September 2009

000_000 Rules Manual

 

 

 

Originator

 

 

SPARK Team

 

 

 

Approver

 

 

SPARK Team Line Manager

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 



Copyright

The contents of this manual are the subject of copyright and all rights in it are reserved.  The manual may not be copied, in whole or in part, without the written consent of Altran Praxis Limited.

 

Limited Warranty

Altran Praxis Limited save as required by law makes no warranty or representation, either express or implied, with respect to this software, its quality, performance, merchantability or fitness for a purpose.  As a result, the licence to use this software is sold ‘as is’ and you, the purchaser, are assuming the entire risk as to its quality and performance.

Altran Praxis Limited accepts no liability for direct, indirect, special or consequential damages nor any other legal liability whatsoever and howsoever arising resulting from any defect in the software or its documentation, even if advised of the possibility of such damages.  In particular Altran Praxis Limited accepts no liability for any programs or data stored or processed using Altran Praxis Limited products, including the costs of recovering such programs or data.

1          Overview

2          Guide To The Built-In Proof Rules

2.1      A Quick Overview Of The Rule Files

2.2      A Summary Of The Built-In Rules

3          Built-In Proof Rules Cross-References

3.1      Quick-Reference Index By Principal Functor

3.2      Index By Rule-Family Name

3.3      Full Expression-Pattern Index

4          Built-In Proof Rule Files

4.1      ARITH.RUL

4.2      ARRAY.RUL

4.3      BITWISE.RUL

4.4      ENUM.RUL

4.5      ENUMERATION.RUL

4.6      FDLFUNCS.RUL

4.7      GENINEQS.RUL

4.8      INTINEQS.RUL

4.9      NUMINEQS.RUL

4.10    LOGIC.RUL

4.11    MODULAR.RUL

4.12    QUANTIF.RUL

4.13    RECORD.RUL

4.14    SEQ.RUL

4.15    SETS.RUL

4.16    SPECIAL.RUL

5          Proof Rule Syntax

5.1      Inference Rules

5.2      Substitution Rules

5.3      Condition Lists

5.4      Permissible Immediate Condition Predicates

5.5      Quantifiers In Proof Rules

5.6      Rule Family Declarations

5.7      Comments In Rule Files

6          Definition And Proof Of Proof Rules

6.1      Definitions

6.2      Properties

6.3      Partiality

6.4      Proofs Of Properties From Definitions

7          Using Buildchlib, The Rule-Library Builder

Document Control and References

File under

Changes history

Changes forecast

Document references

 

 

SPADE is a registered trademark of Altran Praxis Limited.

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


Contents

 

 


1                       Overview

This document provides technical information on the built-in proof rules of the SPADE Proof Checker and describes the process of creating user-defined proof rule files and proof rule libraries.  This Rules Manual is a sister-document to the SPADE Proof Checker User Manual which describes use of the SPADE Proof Checker and its commands.

This document divides naturally into two separate parts: part one is concerned with the built-in proof rules supplied with the Checker, and comprises chapters 2 to 4, while part two, chapters 5 to 6 of this manual, describe how to create your own proof rules and libraries.

Chapter 2 is a guide to the main rule families of the built-in proof rules.  Chapter 3 provides some indices into the built-in rule families, based on the structure of expression in which you are interested and/or rule family name.  Chapter 4 is a complete listing of all the built-in proof rule files.

Chapter 5 describes the syntax of user-defined proof rule files so that you may write your own inference and substitution rules for use with the Checker.  Chapter 6 considers the relationship between definitions of functions and their representation as proof rules, and considers how one may prove that properties of proof rules follow from a definition. 

This manual is intended for both Windows and SUN users of the SPADE Proof Checker.  Where file naming conventions are used, these are mostly in SUN (e.g. /home/user1/ion/myprog.vcg).  Lowercase filenames are assumed throughout, though the built-in rule library uses uppercase names (INTINEQS.RUL).

2                       Guide To The Built-In Proof Rules

2.1               A Quick Overview Of The Rule Files

The Checker’s built-in rule library of approximately 500 proof rules is organised as a collection of rule files.  If the SPADE_CHECKER environment variable is set the Checker will look in this directory for the built-in rule library.  If it is not set, it will look in <root>/lib/checker/rules.  Each rule file has extension .RUL.  Below is a list of the rule files included at present and a quick guide to their contents.

 

ARITH

-

manipulation of arithmetic expressions (by substitution)

ARRAY

-

substitution rules for array-type expressions

BITWISE

-

rules about the functions bit__and(_,_), bit__or(_,_) and bit__xor(_,_)

ENUM

-

rules about enumerated types (pred, succ and ordering)

ENUMERATION

-

additional useful inequalities for enumerated types

FDLFUNCS

-

rules for built-in FDL functions abs(_), sqr(_), odd(_), X**Y

GENINEQS

-

inequalities rules (for integers, reals and enumerated types)

INTINEQS

-

inequalities rules relevant to integers only

NUMINEQS

-

inequalities rules (for integers and reals)

LOGIC

-

rules about the logical operators (and, or, not, ->, <->)

MODULAR

-

rules about modular arithmetic (mod operator)

QUANTIF

-

simple quantifier manipulation rules

SEQ

-

rules about sequence types (length, append, first, last, etc.)

SETS

-

rules about set types (in, not_in, \/, /\, \, subset_of)

RECORD

-

special-invocation rules about record-type objects

SPECIAL

-

special-invocation rules (simplify, standardisation, eq, etc.)

It is useful to have a copy of these rulefiles handy for reference purposes when using the Checker.  They are therefore included in full as chapter 4 of this manual.

In the next section, we shall consider the different “families” of rules in the built-in rule files, as an aid to familiarisation with the rule files.

2.2               A Summary Of The Built-In Rules

In this section, we consider the different rules by family.  Each rule in the built-in rule files has a unique name which is composed of a family name and an instance number, e.g. arith(2) is the second rule of the arith family.  When you use the infer/replace commands, giving the family-name of the rule you think will apply will lead to a faster search of the rulefiles than simply typing a wildcard rule name (though if the rule you need turns out not to be in the family you select, but in another, you will not succeed!).  Obviously, the search will be faster still if you narrow down the search to a subrange of the rule family, or even to a specific rule.  Thus, it is worthwhile to spend some time getting to know the different families of rules available.

2.2.1           Arithmetic rules (mainly in ARITH)

arith

Perform some elementary simplifications e.g.

X*1, 1*X          -->  X      X+0, 0+X    -->  X

X*0,0*X           -->  0      X-0         -->  X

X div 1           -->  X      X/1         -->  X

(X*N) div N       -->  X      (N*X) div N -->  X

(X/Y)*Y           -->  X      (X/Y)*Y     -->  X

(X*Y)/Y           -->  Y      (Y*X)/Y     -->  Y

assoc

Rules for the associativity of + and * (which may only be strictly applied, e.g. a+(b+c) may be rewritten to (a+b)+c, but these rules do not directly allow a+(b-c) to be rewritten to (a+b)-c: the “minus” rules (q.v.) are also needed in this latter case.  This rule family also covers associativity of the logical operators and, or and <-> (in file LOGIC.RUL).

bitwise

(In BITWISE.RUL)  Rules for the bitwise manipulation of modular types using the functions bit__and(_, _), bit__or(_, _) and bit__xor(_, _).

commut

Rules for the commutativity of + and *, so that A op B may be rewritten to B op A.  This rule family also covers commutativity of the logical operators and, or and <-> (in file LOGIC.RUL).

distrib

Rules for the distributivity of * and div over + and -, and for distributivity of the logical operators and over or and or over and.

minus

A batch of rules for manipulating the unary and binary minus operators, e.g. so that A-B may be interchanged with A+(-B), -(-A) may be rewritten as A, etc.

modular

(In MODULAR.RUL)  Rules defining the modular arithmetic operator, mod, and describing some of its properties.

intdiv

Substitution rules about the integer div operator.  Rules include relationship between (A+B) div C and (A div C)+(B div C) when A (or B) is a multiple of C and arithmetic negation within div expressions.

2.2.2           FDL data-type rules (in ARRAY, ENUM, ENUMERATION, SEQ and SETS)

array

Substitution rules about the generic array-manipulation functions element(_,_) and update(_,_,_).  These rules incorporate most of what you need to know about arrays, apart from for proofs of equality of two arrays in some circumstances.  The simplification rules in this family can be performed automatically by the expression simplifier when the simplifier is enabled (with the simplify_during_load and/or simplify_in_infer flags set to on: see section 5.2.7 of the SPADE Proof Checker User Manual for further details of these flags).

mk__array

This is a single rule which allows the user to tell the Checker to simplify element accesses to SPARK array aggregate expressions formed with the mk__array functor.  The expression to be simplified must be of the form element(ARR, [I]), and ARR must be an array aggregate expression, i.e. mk__array(...).  The rationale behind the rule is described in comments preceding the body of the rule.

enum

These rules allow the manipulation of user-defined enumerated types, e.g. by allowing pred(succ(X)) and succ(pred(X)) to be replaced by X (where not at the relevant boundary) and by allowing various inferences about the inherited ordering of the enumerated constants.

enum_cases

This is a family of rules allowing you to infer

X=A1 or X=A2 or ... or X=An

for a variable X of enumerated type T, where

type T = (A1, A2, ..., An)

for some n in 2..25 inclusive.  Rule enum_cases(N) is the rule for an enumeration containing N enumeration constants.

enumeration

This is a family of rules containing additional useful inequalities for enumerated types.  It includes inequalties of the form A < B, A <= B, A > B, A >= B and also such forms involving pred and succ.

seqlen

These rules define the sequence function length(_), giving various substitutions for expressions involving it and some inequalities about it.  (Refer also to section 3.2.6 of the Checker Manual).

append

These rules give properties of the FDL @ (append) operator, thus:

1-2

appending the empty sequence to either side of a list leaves the list unchanged.

3

if A and B are actual lists [a1,...,an], [b1,...,bm], then A @ B is the list [a1,...,an,b1,...,bm].

4-5

a non-empty list S is equal to [first(S)] @ nonfirst(S), and to nonlast(S) @ [last(S)].

6

@ is associative, i.e. (X @ Y) @ Z = X @ (Y @ Z).

first

These rules express properties of the FDL sequence function first(_), thus:

1         first([H,...])     is H

2         first([H,...] @ L) is H

3    first(X @ Y)       is first(X) provided X <> [].

 (N.B. to show first([] @ X) is first(X), use append(1-2) to rewrite [] @ X to X.)

last

These rules express properties of the FDL sequence function last(_), thus:

1    last([H])              is H.

2    last(X @ [H,...])      is   last([H,...]).

3    last([H|T])            is   last(T)  provided T <> [].

4    last(X @ Y)            is   last(Y)  provided Y <> [].

nonfirst

These rules express properties of the FDL sequence function nonfirst(_), thus:

1    nonfirst([H|T])        is T.

2    nonfirst(T)            is []  provided length(T)=1.

3    nonfirst(X @ Y)        is nonfirst(X) @ Y  provided X <> [].

4    nonfirst([H|T] @ Y)    is T @ Y.

nonlast

These rules express properties of the FDL sequence function nonlast(_):

1    nonlast([H])           is [].

2    nonlast(T)             is [] provided length(T)=1.

3    nonlast([H|T])         is [H|T1] provided nonlast(T)=T1.

4    nonlast(X @ Y)         is X @ nonlast(Y) provided Y <> [].

5    nonlast(X @ [H])       is X.

seq

These rules express simple sequence equality properties: that two sequences are equal if and only if they are either both empty or they are both non-empty and have the same first and nonfirst (or last and nonlast) components.

sets

A family of rules for the FDL set operators.  The main groupings are:

(1-3):

simple X in A  &  X not_in A  rules.

(4-11):

properties of set union (\/).

(12-19):

properties of set intersection (/\).

(20-27):

properties of set “lacking” (\).

(28):

X not_in (set []): nothing is in the empty set.

(29-36):

properties of the subset_of relation.

(37):

definition of strict_subset_of relation.

(38-39):

commutativity of \/ and /\.

(40-41):

associativity of \/ and /\.

(42-43):

distributivity of /\ over \/ and \/ over /\.

 

2.2.3           Inequalities rules (mainly in GENINEQS, INTINEQS and NUMINEQS)

inequals

This is a large family of inference rules, covering addition/subtraction to one or both sides of an inequality, multiplication of both sides of an inequality, addition/subtraction of two inequalities and simple inequalities about the div operator.  These rules, together with the Checker’s own inequalities inference capabilities, can cut down on much tedious manipulation, though some may still be necessary on occasion.  This rule family is spread over three files: those in GENINEQS.RUL apply to any ordered type, those in NUMINEQS.RUL apply only to numeric types (i.e. integers and reals) and those in INTINEQS.RUL apply only to integers.  The main groupings are:

 

1-6:

subtraction from one side of inequality (e.g. i-N<j if...)

7-18:

addition to one side of inequality (e.g. i+N>j if...)

19-22:

addition of same no. both sides of <  (e.g. i+N<j+N if...)

23-26:

addition of same no. both sides of >  (e.g. i+N>N+j if...)

27-30:

addition of same no. both sides of <> (e.g. N+i<>N+j if...)

31-33:

subtract same no. both sides </>/<> (e.g. i-N>j-N if...)

34-42:

multiplication both sides by same no. (e.g. i*N<=j*N if...)

43-48:

addition >  :  A+C>B+D  from (A...B or D), (C...D or B)

49-54:

addition <  :  A+C<B+D  from (A...B or D), (C...D or B)

55-60:

addition <> :  A+C<>B+D from (A...B or D), (C...D or B)

61-64:

addition of same no. both sides of =  (e.g. i+N=N+j if...)

65-68:

addition of same no. both sides of <= (e.g. N+i<=j+N if...)

69-72:

addition of same no. both sides of >= (e.g. i+N>=j+N if...)

73-75:

subtract same no. both sides =/<=/>= (e.g. i-N>j-N if...)

76:

I*N=J*N may_be_deduced_from I=J.  (* same no. each side =)

77-79:

addition >= :  A+C>=B+D  from (A...B or D), (C...D or B)

80-82:

addition <= :  A+C>=B+D  from (A...B or D), (C...D or B)

83-85:

addition =  :  A+C>=B+D  from (A...B or D), (C...D or B)

86-87:

lower bounds for N*(A div N) for A>=0, N>0

88-89:

upper bounds for N*(A div N) for A>=0

90-92:

sign of A div N

93-95:

relations between I div N and J div N

96-97:

lower bounds for N*(A div N) for A>=0, N<0

98-100:

sign of A div N

101-103:

strong to weak inequality for integers only

104:

infer X=Y  from X*N=Y*N,  given N<>0

105:

infer X<>Y from X*N<>Y*N, given N<>0

106-107:

infer X<=Y from X*N<=Y*N or X*N>=Y*N depending on sign of N

108-109:

infer X>=Y from X*N>=Y*N or X*N<=Y*N depending on sign of N

110-111:

infer X<Y  from X*N<Y*N  or X*N>Y*N  depending on sign of N

112-113:

infer X>Y  from X*N>Y*N  or X*N<Y*N  depending on sign of N

114-121:

rules about sign of X*Y (<=0, >=0, <0, >0) given signs of X, Y

negation

These rules allow the interchanging of negated inequalities with their counterpart inequalities, e.g. (not a=b) and a<>b.  All of these rules apply to any ordered type, hence their inclusion in GENINEQS.RUL.

strengthen

These rules allow a stronger inequality to be inferred from two weaker ones, e.g. a>=b and a<>b combine to give a>b.  All of these rules apply to any ordered type, hence their inclusion in GENINEQS.RUL.

transitivity

These rules allow the combination of two inequalities to infer a third by transitivity, e.g. from a>b and b>c, we can infer a>c by transitivity, as > is a transitive operator, as are <, =, >= and <= (but not <> in quite the same way).  All of these rules apply to any ordered type, hence their inclusion in GENINEQS.RUL.

To infer X <= Y        try transitivity (1-9)

To infer X >= Y               try transitivity (10-18)

To infer X < Y         try transitivity (19-23)

To infer X > Y         try transitivity (24-28)

To infer X = Y         try transitivity (29)

To infer X <> Y        try transitivity (30)

zero

This is a short family of rules about equality (or otherwise) to zero.  The rules enable one to infer X*Y=0 if either X=0 or Y=0, to infer X=0 or Y=0 from X*Y=0, to infer X*Y<>0 if X<>0 and Y<>0 and to infer X<>0 from X*Y<>0 or from Y*X<>0.

2.2.4           Quantifier rules (in QUANTIF)

quant

A family of rules allowing standard quantifier manipulation of expressions, e.g. changing (not for_all(X,P(X))) into for_some(X,not P(X)), inferring for_some(X,P(X)) from for_some(X,P(X) and Q(X)), etc.

2.2.5           FDL function rules (in FDLFUNCS)

abs

A family of rules giving properties of the FDL abs(_) function.

sqr

Elementary properties of the sqr(X) (“square”, i.e. X*X) function.

odd

A collection of properties of the odd(_) function.

exp

Rules about the ** exponentiation operator added as an extension for Examiner output.  Rules simplifying X**0, 0**X, 1**X, X**1, X**2, X**3, X**4, and defining (-X)**Y in terms of X**Y depending on whether Y is odd, plus recursive rules defining X**(Y+1) in terms of X**Y.  The last six rules of this family allow the sign of X**Y to be inferred from knowledge of the sign of X and, as appropriate, whether or not Y is an odd power.

2.2.6           Logical operator rules (in LOGIC)

logical_not

These rules are elementary simplification rules for not, i.e. that (not true) is false, (not false) is true and (not not X) is X.

logical_and

These rules are elementary simplification rules for and, thus:

X and true   à X            true and X   à X

X and false  à false        false and X  à false

X and not X  à false        not X and X  à false

X and X      à X

logical_or

These rules are elementary simplification rules for or, thus:

X or false  à X             false or X  à X

X or true   à true          true or X   à true

X or not X  à true          not X or X  à true

X or X      à X

implies

These rules are elementary simplification rules for ->, thus:

X -> true   à true          X -> false  à not X

true -> X   à X             false -> X  à true

not X -> X  à X             X -> not X  à not X

X -> X      à true

equivalence

These rules are elementary simplification rules for <->, thus:

X <-> true   à X            true <-> X   à X

X <-> false  à not X        false <-> X  à not X

X <-> not X  à false        not X <-> X  à false

X <-> X      à true

logical

These rules provide other useful rules of classical logic, thus:

not (A or B)  <-> (not A) and (not B)

not (A and B) <-> (not A) or (not B)

A -> B        <-> (not A) or B

A <-> B       <-> (A -> B) and (B -> A)

A -> (B -> C) <-> (A and B) -> C

2.2.7           Special rules (in SPECIAL and RECORD)

eq

This is the equality substitution rule: it allows you to replace A by B provided A=B (and A and B are different expressions).  It is probably the most commonly-used substitution rule.

equiv

This is the equivalence substitution rule: you can use it to replace A by B (or vice versa) provided A <-> B.  It is a special-invocation rule, i.e. you can only apply it if you specifically ask for it: it will not be applied by a wild-card rulename, for instance.

inference

This is a batch of simple rules for inferring compound logical expressions. For example, given a conclusion of the form A or B, this family of rules lets you prove A only, either directly or as a subgoal.  This family of rules can be useful if, for instance, one has a logical expression as a goal, each of whose components are quantified formulae: using this family, the goal may be split into one or more subgoals so that the unwrap command can be used.

logic

These two rules must be invoked with the rulename logic if they are to be used, as without this trigger they will be ignored.  They call the truth-table inference mechanism (used by the deduce command).  One will allow you to infer X if X can be deduced in this way (from no hypotheses, i.e. if it is a truth-table tautology), while the other rule allows you to substitute Y for X if it can deduce that X <-> Y is logically true.

mk__record

These two special-invocation rules give the user access to record aggregate simplification facilities.  The first rule allows a paricular field to be selected from within a SPARK record aggregate expression; it can be used to rewrite expressions of the form fld_F(mk__record(...)) to the value associated with the field F in the aggregate expression.  The second rule allows the user to simplify updates to aggregate expressions: given an expression of the form upf_F(mk__record(...), V), we can rewrite to a new aggregate expression mk__record(...) in which field F is associated with the value of expression V.

record

This family of five rules must be invoked with the rulename record if they are to be used, as without this trigger they will be ignored.  They allow the user to employ the built-in record simplification rules directly to substitute one equivalent expression for another.  Thus, with this rule, the implicit workings of the Checker in manipulating record-type objects can be made explicit where desired.  The rules are:

record(1):

fld_F(upf_F(_, VALUE) may_be_replaced_by VALUE.

record(2):

upf_F(REC, fld_F(REC)) may_be_replaced_by REC.

record(3):

upf_F(upf_G(R, VG), VF) may_be_replaced_by

 upf_G(upf_F(R, VF), VG) if [ “F” <> “G” ].

record(4):

fld_F(upf_G(R, V)) may_be_replaced_by fld_F(R)  

 if [ “F” <> “G” ].

record(5):

upf_F(upf_F(R, _), V) may_be_replaced_by upf_F(R, V).

record_equality

A special-invocation family of rules which allow one to infer that two records are equal if all of their fields are equal, i.e. we can infer that R=S provided we can prove each of fld_field1(R)=fld_field1(S), ... , fld_fieldN(R)=fld_fieldN(S) in turn.

Rules record_equality(1-10) are for records with 1 to 10 fields respectively; rule record_equality(11) deals with records of 11 or more fields in a more general way.

simplify

These two rules must be invoked with the rulename simplify if they are to be used, as without this trigger they will be ignored.  They call the Checker’s built-in expression simplifier directly.  Both rules are substitution rules.  If you provide a determinate expression Y which you wish to substitute for X, this rule will permit the substitution provided both X and Y simplify to the same expression; otherwise, if Y is uninstantiated, the rule will attempt to find the required Y by simplifying X.

standardisation

These three rules must be invoked with the rulename standardisation if they are to be used, as without this trigger they will be ignored.  They call the standardiser directly.  One rule allows you to infer X if X standardises to true.  The other two rules allow substitution.  If you provide a determinate expression Y which you wish to substitute for X, this rule will permit the substitution provided both X and Y have the same standard form; otherwise, if Y is not fully instantiated, the rule will attempt to find the required Y by standardising X.

unification

A special-invocation family of rules which, for any function (or operator) F, allows you to infer F(X1,...,Xn)=F(Y1,...,Yn) from X1=Y1, ..., Xn=Yn (for n in 1..9 at present).

In fact, you can get along without these rules (useful to know if F is a function with 10 or more arguments):  if you want to prove F(X1,...,Xn)=F(Y1,...,Yn) and you can prove X1=Y1, ..., Xn=Yn, then just replace each Yi by Xi in F(X1,...,Xn)=F(Y1,...,Yn) to get the required result; if necessary, you can use proof by contradiction to explicitly introduce the F(Y1,...,Yn) expression first.

3                       Built-In Proof Rules Cross-References

In this chapter, we provide three indices into the built-in proof rule files which were outlined in the previous chapter (and which are listed in full in the following chapter).  The first index in section 3.1 shows, for each principal functor (i.e. main operator or function — the “root” of the expression tree in which you are interested), which rule families may be applicable. The second index in section 3.2 is alphabetically ordered by rule family name and shows, for each rule family, those principal functors for which the family may be of interest and in which rule files the rules are located.  The third index, in section 3.3, is a more comprehensive version of the index in section 3.1: in 3.3, we show not only the principal functor, but also all instances of expression pattern and the rules which are applicable.  Thus, taking rules inequals(18) and inequals(42) as an example, the index in 3.1 records that rule family inequals in NUMINEQS.RUL can be applied to expressions of the form _ <= _ while that in 3.3 records that the inequals rules in NUMINEQS.RUL can be applied to expressions of the form _ <= (_ + _) and of the form (_ * _) <= (_ * _) and other <= patterns (where _ is a place-marker for a general expression).  In this sense, 31 is a “quick-reference” index, while 33 is a more substantial breakdown of relevant expression patterns.

As well as the convention that _ stands for an expression in this index, another convention used in section 3.2 is that an equality enclosed within braces thus — {_ = _} — means that this rule family can only be used for inferring equalities when the use_subst_rules_for_equality flag is set to on; in these circumstances, the equalities which can be inferred will be of the form of subexpressions recorded for that rule family and rule file in section 3.2; we give no further breakdown of these possible equality combinations in section 3.3.  Finally, all ordering was via ASCII sort, though the rule families which apply to general expressions (_) are recorded at the end for the indices in sections 3.1 and 3.3.

The ordering used for the operators in these indices is:

 

*

multiplication

**

exponentiation

+

addition

-

minus (unary, then binary)

->

implication

/

real division

/\

set intersection

<

strictly less-than

<->

logical equivalence

<=

less-than or equal-to

<>

non-equality

=

equality

>

strictly greater-than

>=

greater-than or equal-to

@

sequence append

[_|_]

list notation

\

set lacking

\/

set union

 

 

 

 

 

 

 

 

3.1               Quick-Reference Index By Principal Functor

 

Expression

Rule Families

_ * _

Abs

distrib

Arith

Exp

Assoc

Minus

commut

sqr

_ ** _

exp

 

 

 

_ + _

 

arith

intdiv

assoc

minus

commut

seqlen

distrib

- _

intdiv

Minus

 

 

_ - _

arith

distrib

minus

seqlen

_ > _

implies

Inference

logical

 

_ / _

arith

 

 

 

_ /\ _

sets

 

 

 

_ < _

bitwise

inequals

transitivity

Enum

Modular

enumeration

negation

exp

strengthen

_ <> _

 

 

 

assoc

equivalence

modular

transitivity

commut

Inequals

Negation

Zero

enum

inference

odd

enumeration

logical

seq

_ <= _

 

bitwise

inequals

Enum

Modular

enumeration

negation

exp

transitivity

_ = _

 

 

 

 

 

 

 

 

enum

seq

unification

arith

distrib

implies

logical_and

nonfirst

seqlen

inequals

strengthen

zero

array

equivalence

intdiv

logical_not

nonlast

sets

negation

transitivity

abs

assoc

exp

last

logical_or

quant

sqr

odd

record_equality

append

commut

first

logical

minus

record

modular


_ > _

 

 

abs

inequals

strengthen

Enum

negation

transitivity

enumeration

seqlen

exp

sqr

_ >= _

abs

inequals

transitivity

enum

negation

enumeration

seqlen

exp

sqr

_ @ _

append

nonfirst

nonlast

 

[_|_]

nonlast

 

 

 

_ \ _

sets

 

 

 

_ \/ _

sets

 

 

 

abs(_)

abs

sqr

 

 

_ and _

assoc

logical

commut

logical_and

distrib

inference


Expression

Rule Families

 

 

 

bit__and(_,_)

bitwise

 

 

 

bit__or(_,_)

bitwise

 

 

 

bit__xor(_,)

bitwise

 

 

 

_ div _

arith

intdiv

 

 

Element(_,_)

array

mk__array

 

 

first(_)

first

 

 

 

fld_X(_)

record

mk__record

 

 

for_all(_,_)

quant

 

 

 

for_some(_,_)

quant

 

 

 

_ in _

sets

 

 

 

last(_)

last

 

 

 

length(_)

seqlen

 

 

 

_ mod _

modular

 

 

 

nonfirst(_)

nonfirst

 

 

 

Nonlast(_)

nonlast

 

 

 

not _

 

logical

quant

logical_not

sets

negation

odd

_ not_in _

sets

 

 

 

odd(_)

odd

 

 

 

_ or _

 

abs

enum

logical_or

assoc

enum_cases

quant

commut

inference

sets

distrib

logical

zero

pred(_)

enum   

enumeration

 

 

sqr(_)

sqr

 

 

 

_ strict_subset_of _

sets

 

 

 

_ subset_of _

sets

 

 

 

succ(_)

enum

enumeration

 

 

update(_,_,_)

array

 

 

 

upf_X(_,_)

record

mk__record

 

 

_

 

eq

simplify

equiv

standardisation

inference

logic

 

3.2               Index By Rule-Family Name

 

Rule Family

Rule File

Patterns

abs

 

FDLFUNCS

 

_ * _

abs(_)

_ > _

_ or _

_ >= _

{_ = _}

append

SEQ

_ = _

_ @ _

 

arith

 

ARITH

 

_ * _

_ / _

_ + _

_ div _

_ - _

{_ = _}

array

ARRAY

element(_,_)

update(_,_,_)

{_ = _}

assoc

ARITH

_ * _

_ + _

{_ = _}

assoc

 

LOGIC

 

_ <-> _

_ = _

_ and _

_ or _

bitwise

 

BITWISE

 

_ < _

bit__and(_,_)

_ <= _

bit__or(_,_)

_ = _

bit__xor(_,_)

commut

ARITH

_ * _

_ + _

{_ = _}

commut

LOGIC

_ <-> _

{_ = _}

_ and _

_ or _

distrib

ARITH

_ * _

{_ = _}

_ + _

_ - _

distrib

LOGIC

_ and _

_ or _

{_ = _}

enum

ENUM

 

_ < _

_ = _

_ or _

_ <= _

_ > _

pred(_)

_ <> _

_ >= _

succ(_)

enum_cases

ENUM

_ or _

 

 

enumeration

ENUMERATION

_ <= _

_ > _

pred(_)

_ < _

_ <> _

_ >= _

succ(_)

eq

SPECIAL

_

 

 

equiv

SPECIAL

_

 

 

equivalence

LOGIC

_ <-> _

{_ = _}

 

exp

FDLFUNCS

_ * _

_ <= _

{_ = _}

_ ** _

_ > _

_ < _

_ >= _

first

SEQ

first(_)

{_ = _}

 

implies

LOGIC

_ -> _

{_ = _}

 

inequals

INTINEQS

_ <= _

_ >= _

_ = _

_ > _

inequals

NUMINEQS

 

_ < _

_ = _

_ <= _

_ > _

_ <> _

_ >= _

inference

SPECIAL

_ -> _

_ or _

_ <-> _

_

_ and _

intdiv

ARITH

 

_ + _

{_ = _}

- _

_ div _

last

SEQ

last(_)

{_ = _}

 

logic

SPECIAL

_

 

 

logical

 

LOGIC

_ -> _

not _

_ <-> _

_ or _

_ and _

{_ = _}

logical_and

LOGIC

_ and _

{_ = _}

 

logical_not

LOGIC

not _

{_ = _}

 

logical_or

LOGIC

_ or _

{_ = _}

 

minus

ARITH

_ * _

_ - _

_ + _

{_ = _}

- _

modular

MODULAR

_ < _

_ =_

_ <=_

_ mod _

_ <>_

mk__array

ARRAY

element(_, _)

 

 

mk__record

RECORD

fld_X(_)

upf_X(_, _)

 

negation

GENINEQS

_ < _

_ = _

not _

_ <= _

_ > _

_ <> _

_ >= _

nonfirst

SEQ

_ @ _

nonfirst(_)

{_ = _}

nonlast

SEQ

_ @ _

{_ = _}

[_|_]

nonlast(_)

odd

FDLFUNCS

 

_ <> _

odd(_)

_ = _

not _

quant

QUANTIF

 

for_all(_,_)

_ or _

for_some(_,_)

{_ = _}

not _

record

RECORD

fld_X(_)

upf_X(_,_)

{_ = _}

record_equality

RECORD

_ = _

 

 

seq

SEQ

_ <-> _

_ = _

 

seqlen

SEQ

_ + _

_ >= _

_ - _

length(_)

_ > _

{_ = _}

sets

SETS

_ /\ _

_ in _

_ or _

{_ = _}

_ \ _

not _

_ subset_of _

_ strict_subset_of _

_ \/ _

_ not_in _

simplify

SPECIAL

_

 

 

sqr

FDLFUNCS

_ * _

abs(_)

_ > _

sqr(_)

_ >= _

{_ = _}

standardisation

SPECIAL

_

 

 

strengthen

GENINEQS

_ < _

_ = _

_ > _

transitivity

GENINEQS

 

_ < _

_ = _

_ <= _

_ > _

_ <> _

_ >= _

unification

SPECIAL

_ = _

 

 

zero

NUMINEQS

_ <> _

_ = _

_ or _

 

3.3               Full Expression-Pattern Index

 

Expression

Rule Families

(_ * _) * _

assoc

 

 

(_ + _) * _

distrib

 

 

(- _) * (- _)

minus

 

 

(- _) * _

minus

 

 

(_ - _) * _

distrib

 

 

(_ / _) * _

arith

 

 

0 * _

arith

 

 

1 * _

arith

 

 

_ * (_ * _)

assoc

 

 

_ * (_ ** (_ - 1))

exp

 

 

_ * (_ ** _)

exp

 

 

_ * (_ + _)

distrib

 

 

_ * (- _)

minus

 

 

_ * (_ - _)

distrib

 

 

_ * (_ / _)

arith

 

 

_ * 0

arith

 

 

_ * 1

arith

 

 

_ * _

commut

minus

 

abs(_) * abs(_)

abs

 

 

sqr(_) * sqr(_)

sqr

 

 

(- _) ** _

exp

 

 

0 ** _

exp

 

 

1 ** _

exp

 

 

_ ** (_ + 1)

exp

 

 

_ ** 0

exp

 

 

_ ** 1

exp

 

 

_ ** 2

exp

 

 

_ ** 3

exp

 

 

_ ** 4

exp

 

 

_ ** _

exp

 

 

(_ * _) + (_ * _)

distrib

 

 

(_ + _) + _

assoc

 

 

(- _) + (- _)

minus

 

 

0 + _

arith

 

 

_ + (_ + _)

assoc

 

 

_ + (- _)

minus

 

 

_ + 0

arith

 

 

_ + _

commut

 

 

_ + (_ div _)

intdiv

 

 

(_ div _) + _

intdiv

 

 

(_ div _) + (_ div _)

intdiv

 

 

length(_) + length(_)

seqlen

 

 

length(nonfirst(_)) + 1

seqlen

 

 

length(nonlast(_)) + 1

seqlen

 

 

-(_ * _)

minus

 

 

-(_ + _)

minus

 

 

-(- _)

minus

 

 

-(_ - _)

minus

 

 

-(_ div _)

intdiv

 

 

- 0

minus

 

 

(_ * _) - (_ * _)

distrib

 

 

(- _) - _

minus

 

 

_ - 0

arith

 

 

_ - _

minus

 

 

length(_) - 1

seqlen

 

 

_ -> (_ -> _)

logical

 

 

_ -> _

implies

inference

logical

_ -> false

implies

 

 

_ -> (not _)

implies

 

 

_ -> true

implies

 

 

false -> _

implies

 

 

(not _) -> _

implies

 

 

true -> _

implies

 

 

(_ * _) / _

arith

 

 

_ / 1

arith

 

 

(_ /\ _) /\ _

sets

 

 

(_ \/ _) /\ (_ \/ _)

sets

 

 

_ /\ (_ /\ _)

sets

 

 

_ /\ (_ \/ _)

sets

 

 

_ /\ _

sets

 

 

_ /\ set []

sets

 

 

(set []) /\ _

sets

 

 

(set _) /\ (set _)

sets

 

 

(_ * _) < (_ * _)

inequals

 

 

(_ * _) < 0

inequals

 

 

(_ ** _) < 0

exp

 

 

(_ + _) < (_ + _)

inequals

 

 

(_ - _) < (_ - _)

inequals

 

 

(_ - _) < _

inequals

 

 

_ < (_ + _)

inequals

 

 

_ < _

enum

strengthen

inequals

transitivity

negation

enumeration

_ < _ mod _

modular

 

 

_ mod _ < _

modular

 

 

(_ <-> _) <-> _

assoc

 

 

(_ = _) <-> (... or ...)

seq

 

 

_ <-> (_ <-> _)

assoc

 

 

_ <-> _

commut

logical

equivalence

inference

_ <-> false

equivalence

 

 

_ <-> (not _)

equivalence

 

 

_ <-> true

equivalence

 

 

false <-> _

equivalence

 

 

(not _) <-> _

equivalence

 

 

true <-> _

equivalence

 

 

(_ * _) <= (_ * _)

inequals

 

 

(_ * _) <= 0

inequals

 

 

(_ * (_ div _)) <= _

inequals

 

 

((_ div _) * _) <= _

inequals

 

 

(_ ** _) <= 0

exp

 

 

(_ + 1) <= _

inequals

 

 

(_ + _) <= (_ + _)

inequals

 

 

(_ - _) <= (_ - _)

inequals

 

 

(_ - _) <= _

inequals

 

 

_ <= (_ + _)

inequals

 

 

_ <= _

enum

transitivity

inequals

enumeration

negation

_ mod _ <= _

modular

 

 

_ <= _ mod _

modular

 

 

(_ div _) <= 0

inequals

 

 

(_ + _) <> (_ + _)

inequals

 

 

(_ - _) <> (_ - _)

inequals

 

 

_ <> 0

zero

 

 

_ <> _

enum

inequals

negation

 

transitivity

enumeration

 

(_ * _) = (_ * _)

inequals

 

 

(_ * _) = 0

zero

 

 

((_ div 2) * 2) = _

odd

 

 

(_ + _) = (_ + _)

inequals

 

 

(_ - _) = (_ - _)

inequals

 

 

_ = _

abs

enum

inequals

negation

record_equality

seq

strengthen

transitivity

unification

_ = pred(succ(_))

enum

 

 

_ = succ(pred(_))

enum

 

 

(_ div _) = (_ div _)

inequals

 

 

(_ mod _) = _

modular

 

 

((_ mod _) mod _) =

(_ mod _)

modular

 

 

_ mod _ = -(- _ mod - _)

modular

 

 

pred(succ(_)) = _

enum

 

 

succ(pred(_)) = _

enum

 

 

{_ = _}

append

arith

array

assoc

commut

distrib

equivalence

first

implies

intdiv

last

logical

logical_and

logical_not

logical_or

minus

nonfirst

nonlast

quant

record

seqlen

sets

sqr

 

(_ * _) > (_ * _)

inequals

 

 

(_ * _) > 0

inequals

 

 

(_ ** _) > 0

exp

 

 

(_ + _) > (_ + _)

inequals

 

 

(_ + _) > _

inequals

 

 

(_ div _) <= (_ div _)

inequals

 

 

(_ * _) <> (_ * _)

inequals

 

 

(_ * _) <> 0

zero

 

 

((_ div 2) * 2) <> _

odd

 

 

(_ - _) > (_ - _)

inequals

 

 

_ > (_ - _)

inequals

 

 

_ > _

enum

inequals

negation

strengthen

transitivity

enumeration

abs(_) > 0

abs

 

 

(_ div _) > 0

inequals

 

 

length([_|_]) > 0

seqlen

 

 

sqr(_) > 0

sqr

 

 

(_ * _) >= (_ * _)

inequals

 

 

(_ * _) >= 0

inequals

 

 

_ * _ div _ >= _ + _ + 1

inequals

 

 

_ * _ div _ >= _ - _ + 1

inequals

 

 

_ div _ * _ >= _ + _ + 1

inequals

 

 

_ div _ * _ >= _ - _ + 1

inequals

 

 

(_ ** _) >= 0

exp

 

 

(_ + _) >= (_ + _)

inequals

 

 

(_ + _) >= _

inequals

 

 

(_ - _) >= (_ - _)

inequals

 

 

_ >= (_ + 1)

inequals

 

 

_ >= (_ - _)

inequals

 

 

_ >= 1

inequals

 

 

_ >= _

enum transitivity

inequals enumeration

negation

abs(_) >= 0

abs

 

 

(_ div _) >= 0

inequals

 

 

(_ div _)  >= (_ div _)

inequals

 

 

length([_|_]) >= 1

seqlen

 

 

length(_) >= 0

seqlen

 

 

sqr(_) >= 0

sqr

 

 

(_ @ _) @ _

append

 

 

[] @ _

append

 

 

[_|_] @ [_|_]

append

 

 

[first(_)] @ nonfirst(_)

append

 

 

_ @ (_ @ _)

append

 

 

_ @ []

append

 

 

_ @ nonlast(_)

nonlast

 

 

nonfirst(_) @ _

nonfirst

 

 

nonlast(_) @ [last(_)]

append

 

 

[_|_]

nonlast

 

 

_ \ _

sets

 

 

(set _) \ (set _)

sets

 

 

(_ /\ _) \/ (_ /\ _)

sets

 

 

(_ \/ _) \/ _

sets

 

 

_ \/ (_ /\ _)

sets

 

 

_ \/ (_ \/ _)

sets

 

 

_ \/ (set [])

sets

 

 

(set []) \/ _

sets

 

 

(set _) \/ (set _)

sets

 

 

abs(_ * _)

abs

 

 

abs(_)

abs

 

 

abs(abs(_))

abs

 

 

abs(sqr(_))

sqr

 

 

(_ -> _) and (_ -> _)

logical

 

 

_ and _

commut

inference

logical_and

_ and (_ and _)

assoc

 

 

_ and false

logical_and

 

 

_ and (not _)

logical_and

 

 

_ and (_ or _)

distrib

 

 

_ and true

logical_and

 

 

(_ and _) and _

assoc

 

 

false and _

logical_and

 

 

(not _) and _

logical_and

 

 

(not _) and (not _)

logical

 

 

(_ or _) and _

distrib

 

 

(_ or _) and (_ or _)

distrib

 

 

true and _

logical_and

 

 

(_ * _) div (_ * _)

intdiv

 

 

(_ * _) div _

arith

intdiv

 

(_ + _) div _

intdiv

 

 

(- _) div (- _)

intdiv

 

 

(- _) div _

intdiv

 

 

_ div (- _)

intdiv

 

 

_ div 1

arith

 

 

_ div _

intdiv

 

 

element(_,_)

array

 

 

element(mk__array(_),_)

mk__array

 

 

element(update(_,_,_),_)

array

 

 

first([_|_] @ _)

first

 

 

first(_ @ _)

first

 

 

first([_|_])

first

 

 

first(_)

first

 

 

fld_X(mk__record(_..._))

mk__record

 

 

fld_X(upf_X(_,_))

record

 

 

fld_X(upf_Y(_,_))

record

 

 

for_all(_,_ -> _)

quant

 

 

for_all(_,_ <-> _)

quant

 

 

for_all(_,_)

quant

 

 

for_all(_,_ and _)

quant

 

 

for_all(_,for_all(_,_))

quant

 

 

for_all(_,(not _))

quant

 

 

for_all(_,_ or _)

quant

 

 

for_some(_,_ -> _)

quant

 

 

for_some(_,_)

quant

 

 

for_some(_,for_all(_,_))

quant

 

 

for_some(_,for_some(_,_))

quant

 

 

for_some(_,(not _))

quant

 

 

for_some(_,_ or _)

quant

 

 

_ in (_ /\ _)

sets

 

 

_ in (_ \ _)

sets

 

 

_ in (_ \/ _)

sets

 

 

_ in _

sets

 

 

_ in (set _)

sets

 

 

last(_ @ [_|_])

last

 

 

last(_ @ _)

last

 

 

last([_])

last

 

 

last([_|_])

last

 

 

last(_)

last

 

 

length(_ @ _)

seqlen     

 

 

length([])

seqlen

 

 

length([_|_])

seqlen

 

 

length(_)

seqlen

 

 

length(nonfirst(_))

seqlen

 

 

length(nonlast(_))

seqlen

 

 

_ mod _

modular

 

 

(_ * _) mod _

modular

 

 

(_ mod _) mod _

modular

 

 

nonfirst([_|_] @ _)

nonfirst

 

 

nonfirst(_ @ _)

nonfirst

 

 

nonfirst([_|_])

nonfirst

 

 

nonfirst(_)

nonfirst

 

 

nonlast(_ @ [_])

nonlast

 

 

nonlast(_ @ _)

nonlast

 

 

nonlast([_])

nonlast

 

 

nonlast([_|_])

nonlast

 

 

nonlast(_)

nonlast

 

 

not (_ < _)

negation

 

 

not (_ <= _)

negation

 

 

not (_ <> _)

negation

 

 

not (_ = _)

negation

 

 

not (_ > _)

negation

 

 

not (_ >= _)

negation

 

 

not (_ and _)

logical

 

 

not false

logical_not

 

 

not for_all(_,_)

quant

 

 

not for_all(_,(not _))

quant

 

 

not for_some(_,_)

quant

 

 

not for_some(_,(not _))

quant

 

 

not (_ in _)

sets

 

 

not (not _)

logical_not

 

 

not (_ not_in _)

sets

 

 

not odd(_ * _)

odd

 

 

not odd(_ + _)

odd

 

 

not odd(- _)

odd

 

 

not odd(_ - _)

odd

 

 

not odd(_)

odd

 

 

not odd(abs(_))

odd

 

 

not odd(sqr(_))

odd

 

 

not (_ or _)

logical

 

 

not true

logical_not

 

 

_ not_in (_ /\ _)

sets

 

 

_ not_in (_ \ _)

sets

 

 

_ not_in (_ \/ _)

sets

 

 

_ not_in _

sets

 

 

_ not_in (set [])

sets

 

 

odd(_ * _)

odd

 

 

odd(_ + _)

odd

 

 

odd(- _)

odd

 

 

odd(_ - _)

odd

 

 

odd(_)

odd

 

 

odd(abs(_))

odd

 

 

odd(sqr(_))

odd

 

 

(_ = 0) or (_ = 0)

zero

 

 

(_ = _) or (_ = _)

enum_cases

 

 

(_ = _) or (_ >= _)

enum

 

 

(_ = _) or _

enum

 

 

(_ = _) or _

enum_cases

 

 

(_ = _) or (_ in _)

sets

 

 

abs(_)=_ or abs(_)=(- _)

abs

 

 

_ or _

commut

inference

logical_or

_ or (_ and _)

distrib

 

 

_ or false

logical_or

 

 

_ or (not _)

logical_or

 

 

_ or (_ or _)

assoc

 

 

_ or true

logical_or

 

 

(_ and _) or _

distrib

 

 

(_ and _) or (_ and _)

distrib

 

 

false or _

logical_or

 

 

for_some(_,_) or ...

quant

 

 

(not _) or _

logical

logical_or

 

(not _) or (not _)

logical

 

 

(_ or _) or _

assoc

 

 

true or _

logical_or

 

 

pred(_)

enum

enumeration

 

sqr(_ * _)

sqr

 

 

sqr(_)

sqr

 

 

sqr(abs(_))

sqr

 

 

_ strict_subset_of _

sets

 

 

(_ /\ _) subset_of _

sets

 

 

(_ \ _) subset_of _

sets

 

 

_ subset_of (_ \/ _)

sets

 

 

_ subset_of _

sets

 

 

(set []) subset_of _

sets

 

 

(set _) subset_of (set _)

sets

 

 

succ(_)

enum

enumeration

 

update(_,_,element (_,_))

array

 

 

update(update(_,_,_),_,_)

array

 

 

upf_X(_,fld_X(_))

record

 

 

upf_X(mk__record(_),_)

mk__record

 

 

upf_X(upf_X(_,_),_)

record

 

 

upf_X(upf_Y(_,_),_)

record

 

 

_

eq

logic

equiv

simplify

inference

standardisation

 

 

 

 

 

 

4                       Built-In Proof Rule Files

4.1               ARITH.RUL

%-------------------------------------------------------------------------------

%  (C) Altran Praxis Limited

%-------------------------------------------------------------------------------

%

%  The SPARK toolset is free software; you can redistribute it and/or modify it

%  under terms of the GNU General Public License as published by the Free

%  Software Foundation; either version 3, or (at your option) any later

%  version. The SPARK toolset is distributed in the hope that it will be

%  useful, but WITHOUT ANY WARRANTY; without even the implied warranty of

%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General

%  Public License for more details. You should have received a copy of the GNU

%  General Public License distributed with the SPARK toolset; see file

%  COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of

%  the license.

%

%===============================================================================

 

 

%-------------------------------------------------------------------------------

% RULE FAMILIES CONTAINED HEREIN :-

%

% arith        : simple arithmetic simplification rules

% assoc        : associativity of + and *

% commut       : commutativity of + and *

% distrib      : distributivity of * over + and -

% minus        : rules for unary and binary minus

% intdiv       : rules for the integer div operator

%-------------------------------------------------------------------------------

% MODEL DECLARATIONS FOR THIS FILE :-

%

% rule_family arith:

%         X * Y   requires [ X:ir, Y:ir ] &

%         X + Y   requires [ X:ir, Y:ir ] &

%         X - Y   requires [ X:ir, Y:ir ] &

%         X div Y requires [ X:i,  Y:i  ] &

%         X / Y   requires [ X:ir, Y:ir ].

%

% rule_family assoc:

%         X + Y requires [ X:ir, Y:ir ] &

%         X * Y requires [ X:ir, Y:ir ].

%

% rule_family commut:

%         X + Y requires [ X:ir, Y:ir ] &

%         X * Y requires [ X:ir, Y:ir ].

%

% rule_family distrib:

%         X + Y requires [ X:ir, Y:ir ] &

%         X - Y requires [ X:ir, Y:ir ] &

%         X * Y requires [ X:ir, Y:ir ].

%

% rule_family minus:

%         - X   requires [ X:ir       ] &

%         X + Y requires [ X:ir, Y:ir ] &

%         X - Y requires [ X:ir, Y:ir ] &

%         X * Y requires [ X:ir, Y:ir ].

%

% rule_family intdiv:

%         X div Y requires [ X:i, Y:i ] &

%         X + Y   requires [ X:i, Y:i ] &

%         - X     requires [ X:i      ].

%-------------------------------------------------------------------------------

/*** SIMPLIFICATION OF ARITHMETIC EXPRESSIONS Rules ***/

 

arith(1):    X*1             may_be_replaced_by X.

arith(2):    1*X             may_be_replaced_by X.

arith(3):    X+0             may_be_replaced_by X.

arith(4):    0+X             may_be_replaced_by X.

arith(5):    X - 0           may_be_replaced_by X.

arith(6):    X*0             may_be_replaced_by 0.

arith(7):    0*X             may_be_replaced_by 0.

arith(8):    X div 1         may_be_replaced_by X.

arith(9):    (X*N) div N     may_be_replaced_by X        if [ N<>0 ].

arith(10):   (N*X) div N     may_be_replaced_by X        if [ N<>0 ].

arith(11):    X/1            may_be_replaced_by X.

arith(12):    (X/Y)*Y        may_be_replaced_by X        if [ Y<>0 ].

arith(13):    Y*(X/Y)        may_be_replaced_by X        if [ Y<>0 ].

arith(14):    (X*Y)/Y        may_be_replaced_by X        if [ Y<>0 ].

arith(15):    (Y*X)/Y        may_be_replaced_by X        if [ Y<>0 ].

 

 

/*** ASSOCIATIVITY of + & * Rules ***/

 

assoc(1):       (A+B)+C         may_be_replaced_by A+(B+C).

assoc(2):       A+(B+C)         may_be_replaced_by (A+B)+C.

assoc(3):       (A*B)*C         may_be_replaced_by A*(B*C).

assoc(4):       A*(B*C)         may_be_replaced_by (A*B)*C.

 

 

/*** COMMUTATIVITY of + & * Rules ***/

 

commut(1):      A+B             may_be_replaced_by B+A.

commut(2):      A*B             may_be_replaced_by B*A.

 

 

/*** DISTRIBUTIVITY of * over + & - Rules ***/

 

distrib(1):   A*(B+C) & A*B+A*C are_interchangeable.

distrib(2):   (B+C)*A & A*B+A*C are_interchangeable.

distrib(3):   A*(B-C) & A*B-A*C are_interchangeable.

distrib(4):   (B-C)*A & A*B-A*C are_interchangeable.

 

 

/*** Rules for manipulation of unary and binary MINUS operators ***/

 

minus(1):       X-X                      may_be_replaced_by 0.

minus(2):       -(0)                     may_be_replaced_by 0.

minus(3):       -(-X)                    may_be_replaced_by X.

minus(4):       -(A+B) & -A+(-B)         are_interchangeable.

minus(5):       -(A+B) & -A-B            are_interchangeable.

minus(6):       -A+(-B) & -A-B           are_interchangeable.

minus(7):       A+(-B) & A-B             are_interchangeable.

minus(8):       A+(-B) & -(B-A)          are_interchangeable.

minus(9):       A-B & -(B-A)             are_interchangeable.

minus(10):      -A*B & A*(-B)            are_interchangeable.

minus(11):      -A*B & -(A*B)            are_interchangeable.

minus(12):      -(A*B) & A*(-B)          are_interchangeable.

minus(13):      -A*(-B) & A*B            are_interchangeable.

 

 

/*** Some rules for INTEGER DIVISION ***/

 

intdiv(1):   (A+B) div C & A div C+B div C are_interchangeable

                     if [B=K*C, A*B>=0].

intdiv(2):   (A+B) div C & A div C+B div C are_interchangeable

                     if [B=C*K, A*B>=0].

intdiv(3):   (A+B) div C & A div C+B div C are_interchangeable

                     if [A=K*C, A*B>=0].

intdiv(4):   (A+B) div C & A div C+B div C are_interchangeable

                     if [A=C*K, A*B>=0].

intdiv(5):   (A+B) div C & A div C+D       are_interchangeable

                     if [goal(integer(B)), goal(integer(C)), goal(C\=0),

                         goal(D iss B div C), goal(B iss D*C), A*B>=0].

intdiv(6):   (A+B) div C & D+B div C       are_interchangeable

                             if [goal(integer(A)), goal(integer(C)), goal(C\=0),

                                 goal(D iss A div C), goal(A iss D*C), A*B>=0].

intdiv(7):   -A div B    & A div (-B)      are_interchangeable.

intdiv(8):   -A div B    & -(A div B)      are_interchangeable.

intdiv(9):   A div (-B)  & -(A div B)      are_interchangeable.

intdiv(10):  -A div (-B) & A div B         are_interchangeable.

intdiv(11):  (A*B) div B                 may_be_replaced_by A if [B<>0].

intdiv(12):  (A*B) div (C*B)             may_be_replaced_by A div C if [B<>0].


4.2               ARRAY.RUL

%-------------------------------------------------------------------------------

%  (C) Altran Praxis Limited

%-------------------------------------------------------------------------------

%

%  The SPARK toolset is free software; you can redistribute it and/or modify it

%  under terms of the GNU General Public License as published by the Free

%  Software Foundation; either version 3, or (at your option) any later

%  version. The SPARK toolset is distributed in the hope that it will be

%  useful, but WITHOUT ANY WARRANTY; without even the implied warranty of

%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General

%  Public License for more details. You should have received a copy of the GNU

%  General Public License distributed with the SPARK toolset; see file

%  COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of

%  the license.

%

%===============================================================================

 

 

%-------------------------------------------------------------------------------

% RULE FAMILY CONTAINED HEREIN :-

% array        : basic properties of FDL array manipulation functions

% mk__array    : rules specific to SPARK array aggregates

%-------------------------------------------------------------------------------

% MODEL DECLARATION FOR THIS FILE :-

%

% rule_family array:

%         element(X, Y)   requires [ X:any, Y:any        ] &

%         update(X, Y, Z) requires [ X:any, Y:any, Z:any ].

%

% rule_family mk__array:

%         element(X, Y)   requires [ X:any, Y:any ].

%-------------------------------------------------------------------------------

 

/*** Rules specific to ARRAY MANIPULATIONS ***/

 

array(1):  element(update(A,I,X),I) may_be_replaced_by X.

array(2):  update(A,I,element(A,I)) may_be_replaced_by A.

array(3):  element(update(A,J,X),K) & element(A,K) are_interchangeable if

                [ J<>K ].

array(4):  update(update(A,I,X),J,Y) & update(update(A,J,Y),I,X)

                are_interchangeable if [ I<>J ].

array(5):  update(update(A,I,X),I,Y) may_be_replaced_by update(A,I,Y).

 

 

/*** Rules specific to SPARK ARRAY AGGREGATES ***/

 

/* mk__array(1):

       element(mk__array(LARGS, Inds := X), [I]) may_be_replaced_by X if

              [ "satisfies_index_constraint(Inds, I)" ].

   In the above rule, the quoted side-condition can be met as follows:

       (1) if Inds is of the form "[J]", by satisfying I = J;

       (2) if Inds is of the form "[J .. K]", by satisfying J <= I <= K;

       (3) if Inds is of the form "Is & Js", by satisfying either Is or Js.

   Note that the last case makes the definition recursive.

 

   Equally, if we can prove that I does not satisfy the index constraints

   represented by Inds, we can instead consider whether it satisfies any of

   the index constraints in LARGS, and so on recursively until we either

   succeed or reach a point where neither satisfaction nor non-satisfaction can

   be proved (because of an insufficiently powerful inference engine, for

   instance, or because the index I is insufficiently constrained by the

   hypotheses of the VC).

 

   Given the above, the following is a general-purpose rule for fetching the

   value of an element of an array aggregate (where this is non-trivial): */

 

mk__array(1):

       element(MK__ARRAY_PART, [I]) may_be_replaced_by VALUE if

              [ goal(nonvar(MK__ARRAY_PART)),

                goal(MK__ARRAY_PART =.. [mk__array|ARGUMENTS]),

                goal(find_element(MK__ARRAY_PART, [I], VALUE)) ].

 

 

/* mk__array(2):

       element(mk__ARRAYTYPE(LARGS, Inds := X), [I]) may_be_replaced_by X if

              [ "satisfies_index_constraint(Inds, I)" ].

   In the above rule, the quoted side-condition can be met as follows:

       (1) if Inds is of the form "[J]", by satisfying I = J;

       (2) if Inds is of the form "[J .. K]", by satisfying J <= I <= K;

       (3) if Inds is of the form "Is & Js", by satisfying either Is or Js.

   Note that the last case makes the definition recursive.

 

   Given the above, the following is a general-purpose rule for fetching the

   value of an element of a typed array aggregate (where non-trivial): */

 

mk__array(2):

       element(MK__ARRAY_PART, [I]) may_be_replaced_by VALUE if

              [ goal(nonvar(MK__ARRAY_PART)),

                goal(MK__ARRAY_PART =.. [MK__ARRAYTYPE|ARGUMENTS]),

                goal(mk__function_name(MK__ARRAYTYPE, _, array)),

                goal(find_element(MK__ARRAY_PART, [I], VALUE)) ].

 

 

/* It is recommended that the user should avoid reasoning about the

   equality (or otherwise) of two array aggregates. */


4.3               BITWISE.RUL

%-------------------------------------------------------------------------------

%  (C) Altran Praxis Limited

%-------------------------------------------------------------------------------

%

%  The SPARK toolset is free software; you can redistribute it and/or modify it

%  under terms of the GNU General Public License as published by the Free

%  Software Foundation; either version 3, or (at your option) any later

%  version. The SPARK toolset is distributed in the hope that it will be

%  useful, but WITHOUT ANY WARRANTY; without even the implied warranty of

%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General

%  Public License for more details. You should have received a copy of the GNU

%  General Public License distributed with the SPARK toolset; see file

%  COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of

%  the license.

%

%===============================================================================

 

 

%-------------------------------------------------------------------------------

% RULE FAMILIES CONTAINED HEREIN :-

% bitwise : bitwise logical operators for SPARK Modular Types

%-------------------------------------------------------------------------------

% MODEL DECLARATIONS FOR THIS FILE :-

%

% rule_family bitwise:

%      bit__and(I,J) requires [I : i, J : i] &

%      bit__or(I,J)  requires [I : i, J : i] &

%      bit__xor(I,J) requires [I : i, J : i] &

%      bit__and(I,J) = K requires [I : i, J : i, K : i] &

%      bit__or(I,J)  = K requires [I : i, J : i, K : i] &

%      bit__xor(I,J) = K requires [I : i, J : i, K : i] &

%      I < J         requires [I : i, J : i] &

%      I <= J        requires [I : i, J : i] &

%      I = J         requires [I : i, J : i].

%-------------------------------------------------------------------------------

 

/*** Simplification of bitwise operators ***/

bitwise(1):      bit__and(X,X)         may_be_replaced_by X if [ 0 <= X ].

bitwise(2):      bit__or(X,X)          may_be_replaced_by X if [ 0 <= X ].

bitwise(3):      bit__xor(X,X)         may_be_replaced_by 0 if [ 0 <= X ].

bitwise(4):      bit__and(X, 2**N - 1) may_be_replaced_by X if [ 0 <= X, 0 <= N,

                                                                 X <= 2**N - 1 ].

/*** Properties of zero ***/

bitwise(11):     bit__and(X,0)        may_be_replaced_by    0    if [ 0 <= X ].

bitwise(12):     bit__or(X,0)         may_be_replaced_by    X    if [ 0 <= X ].

bitwise(13):     bit__xor(X,0)        may_be_replaced_by    X    if [ 0 <= X ].

 

/*** Commutativity ***/

bitwise(21):     bit__and(X,Y)        may_be_replaced_by

                                           bit__and(Y,X) if [ 0 <= X, 0 <= Y ].

bitwise(22):     bit__or(X,Y)         may_be_replaced_by

                                           bit__or(Y,X)  if [ 0 <= X, 0 <= Y ].

bitwise(23):     bit__xor(X,Y)        may_be_replaced_by

                                           bit__xor(Y,X) if [ 0 <= X, 0 <= Y ].

 

/*** Associativity ***/

bitwise(31):     bit__and(bit__and(X,Y), Z) may_be_replaced_by

                              bit__and(bit__and(X,Z), Y) if [ 0 <= X, 0 <= Y ].

bitwise(32):     bit__or(bit__or(X,Y), Z)   may_be_replaced_by

                              bit__or(bit__or(X,Z), Y)   if [ 0 <= X, 0 <= Y ].

bitwise(33):     bit__xor(bit__xor(X,Y), Z) may_be_replaced_by

                              bit__xor(bit__xor(X,Z), Y) if [ 0 <= X, 0 <= Y ].

 

/*** Distributivity of bit__and and bit__or (bit__xor requires negation)***/

bitwise(41):    bit__or(bit__and(X,Y), Z) & bit__and(bit__or(X,Z), bit__or(Y,Z))

                             are_interchangeable if [ 0 <= X, 0 <= Y, 0 <= Z ].

bitwise(42):    bit__and(bit__or(X,Y), Z) & bit__or(bit__and(X,Z), bit__and(Y,Z))

                             are_interchangeable if [ 0 <= X, 0 <= Y, 0 <= Z ].

 

/*** Lower bounds ***/

bitwise(51):    0 <= bit__and(X,Y)      may_be_deduced_from  [ 0 <= X, 0 <= Y ].

bitwise(52):    0 <= bit__or(X,Y)       may_be_deduced_from  [ 0 <= X, 0 <= Y ].

bitwise(53):    0 <= bit__xor(X,Y)      may_be_deduced_from  [ 0 <= X, 0 <= Y ].

bitwise(54):    X <= bit__or(X,Y)       may_be_deduced_from  [ 0 <= X, 0 <= Y ].

bitwise(55):    Y <= bit__or(X,Y)       may_be_deduced_from  [ 0 <= X, 0 <= Y ].

bitwise(56):    X - Y <= bit__xor(X, Y) may_be_deduced_from  [ 0 <= X, 0 <= Y ].

bitwise(57):    Y - X <= bit__xor(X, Y) may_be_deduced_from  [ 0 <= X, 0 <= Y ].

 

/*** Upper bounds ***/

bitwise(61):  bit__and(X,Y) <= X         may_be_deduced_from [ 0 <= X, 0 <= Y ].

bitwise(62):  bit__and(X,Y) <= Y         may_be_deduced_from [ 0 <= X, 0 <= Y ].

bitwise(63):  bit__or(X,Y)  <= X + Y     may_be_deduced_from [ 0 <= X, 0 <= Y ].

bitwise(64):  bit__xor(X,Y) <= X + Y     may_be_deduced_from [ 0 <= X, 0 <= Y ].

bitwise(65):  bit__and(X,Y) <= Z         may_be_deduced_from [ 0 <= X, 0 <= Y,

                                                               X <= Z or Y <= Z].

bitwise(66):  bit__or(X,Y) <= 2**N - 1   may_be_deduced_from [ 0 <= X, 0 <= Y,

                                                               0 <= N,

                                                               X <= 2**N - 1,

                                                               Y <= 2**N - 1 ].

bitwise(67):  bit__xor(X,Y) <= 2**N - 1  may_be_deduced_from [ 0 <= X, 0 <= Y,

                                                               0 <= N,

                                                               X <= 2**N - 1,

                                                               Y <= 2**N - 1].

 

/*** Values ***/

bitwise(72):      bit__or(X,Y)  may_be_replaced_by X + Y - bit__and(X,Y)

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

bitwise(73):      bit__xor(X,Y) may_be_replaced_by X + Y - 2 * bit__and(X,Y)

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

 

/*** Comparison ***/

bitwise(81):     bit__and(X,Y) <= bit__or(X,Y) may_be_deduced_from

                                                      [ 0 <= X, 0 <= Y].

bitwise(82):     bit__xor(X,Y) <= bit__or(X,Y) may_be_deduced_from

                                                      [ 0 <= X, 0 <= Y].

 

 

/*** Combination of X with ~X ***/

bitwise(91):     bit__and(X, 2**N - X - 1) = 0        may_be_deduced_from

                                               [ 0 <= X, 0 <= N, X <= 2**N - 1 ].

bitwise(92):     bit__or(X, 2**N - X - 1) = 2**N - 1  may_be_deduced_from

                                               [ 0 <= X, 0 <= N, X <= 2**N - 1 ].

bitwise(93):     bit__xor(X, 2**N - X - 1) = 2**N - 1 may_be_deduced_from

                                               [ 0 <= X, 0 <= N, X <= 2**N - 1 ].

 

/*** Maximum value argument ***/

bitwise(101):     bit__and(X, 2**N - 1) = 2**N - 1     may_be_deduced_from

                                               [ 0 <= X, 0 <= N, X <= 2**N - 1 ].

bitwise(102):     bit__or(X, 2**N - 1)  = 2**N - 1     may_be_deduced_from

                                               [ 0 <= X, 0 <= N, X <= 2**N - 1 ].

bitwise(103):     bit__xor(X, 2**N - 1) = 2**N - X - 1 may_be_deduced_from

                                               [ 0 <= X, 0 <= N, X <= 2**N - 1 ].

/*** Definition of bit__and ***/

bitwise(111): bit__and(X, Y) may_be_replaced_by 2 * bit__and(X div 2, Y div 2) +

                                      (X mod 2) * (Y mod 2) if [0 <= X, 0 <= Y ].


4.4               ENUM.RUL

%-------------------------------------------------------------------------------

%  (C) Altran Praxis Limited

%-------------------------------------------------------------------------------

%

%  The SPARK toolset is free software; you can redistribute it and/or modify it

%  under terms of the GNU General Public License as published by the Free

%  Software Foundation; either version 3, or (at your option) any later

%  version. The SPARK toolset is distributed in the hope that it will be

%  useful, but WITHOUT ANY WARRANTY; without even the implied warranty of

%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General

%  Public License for more details. You should have received a copy of the GNU

%  General Public License distributed with the SPARK toolset; see file

%  COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of

%  the license.

%

%===============================================================================

%-------------------------------------------------------------------------------

% RULE FAMILIES CONTAINED HEREIN :-

%

% enum         : properties of enumerated types (pred & succ etc.)

% enum_cases   : list of cases for enumerations of size 2..25 elements

%-------------------------------------------------------------------------------

% MODEL DECLARATIONS FOR THIS FILE :-

%

% rule_family enum:

%         X = Y   requires [ X:e,   Y:e   ] &

%         X <= Y  requires [ X:e,   Y:e   ] &

%         X < Y   requires [ X:e,   Y:e   ] &

%         X >= Y  requires [ X:e,   Y:e   ] &

%         X > Y   requires [ X:e,   Y:e   ] &

%         X <> Y  requires [ X:e,   Y:e   ] &

%         X or Y  requires [ X:any, Y:any ] &

%         succ(X) requires [ X:e          ] &

%         pred(X) requires [ X:e          ].

%

% rule_family enum_cases:

%         X or Y requires [ X:any, Y:any ].

%-------------------------------------------------------------------------------

 

/*** Enumerated type rules ***/

 

enum(1):        pred(succ(X))=X may_be_deduced_from

                        [ goal(enumeration_list(X,L)),

                          goal(\+ last(L,X)) ].

enum(2):        X=pred(succ(X)) may_be_deduced_from

                        [ goal(enumeration_list(X,L)),

                          goal(\+ last(L,X)) ].

enum(3):        succ(pred(X))=X may_be_deduced_from

                        [ goal(enumeration_list(X,L)),

                          goal(L\=[X|_]) ].

enum(4):        X=succ(pred(X)) may_be_deduced_from

                        [ goal(enumeration_list(X,L)),

                          goal(L\=[X|_]) ].

enum(5):        X <= Y may_be_deduced_from

                        [ goal(enumeration_list(X,L)),

                          goal(in_order(X,Y,L)) ].

enum(6):        X < Y may_be_deduced_from

                        [ goal(enumeration_list(X,L)),

                          goal(in_order(X,Y,L)), goal(X\=Y) ].

enum(7):        Y >= X may_be_deduced_from

                        [ goal(enumeration_list(X,L)),

                          goal(in_order(X,Y,L)) ].

enum(8):        Y > X may_be_deduced_from

                        [ goal(enumeration_list(X,L)),

                          goal(in_order(X,Y,L)), goal(X\=Y) ].

enum(9):        X<>Y may_be_deduced_from

                        [ goal(enumeration_list(X,L)), goal(is_in(X,L)),

                          goal(is_in(Y,L)), goal(X\=Y) ].

enum(10):       X=E may_be_deduced_from

                        [ X<=E, goal(enumeration_list(E,[E|_])) ].

enum(11):       X=E may_be_deduced_from

                        [ X<F, goal(enumeration_list(F,[E,F|_])) ].

enum(12):       X=E may_be_deduced_from

                       [ X>=E, goal(enumeration_list(E,L)), goal(last(L,E)) ].

enum(13):       X=E may_be_deduced_from

                        [ X>F, goal(enumeration_list(E,L)), goal(last(L,E)),

                          goal(sublist([F,E],L)) ].

enum(14):       X=E1 or X>=E2 may_be_deduced_from

                        [ X>=E1, goal(enumeration_list(E1,L)),

                          goal(sublist([E1,E2],L)) ].

enum(15):       X=E or REST may_be_deduced_from

                        [ goal(atom(E)), goal(enumeration_list(E,L)),

                          goal(build_other_cases(X,E,L,REST)),

                          goal(REST\=false) ].

enum(16):       X=E may_be_deduced_from

                        [ goal(atom(E)), goal(enumeration_list(E,L)),

                          goal(build_other_cases(X,E,L,false)) ].

enum(17):       succ(Y) may_be_replaced_by X if

                        [ goal(enumeration_list(Y,L)),

                          goal(sublist([Y,X],L)) ].

enum(18):       pred(X) may_be_replaced_by Y if

                        [ goal(enumeration_list(X,L)),

                          goal(sublist([Y,X],L)) ].

 

 

enum_cases(2):  X=A or X=B may_be_deduced_from

                       [ goal(atom(X)),

                         goal(checktype(X,TYPE)),

                         goal(type(TYPE,enumerated)),

                         goal(enumeration(TYPE,[A,B])) ].

enum_cases(3):  X=A or X=B or X=C may_be_deduced_from

                       [ goal(atom(X)),

                         goal(checktype(X,TYPE)),

                         goal(type(TYPE,enumerated)),

                         goal(enumeration(TYPE,[A,B,C])) ].

enum_cases(4):  X=A or X=B or X=C or X=D may_be_deduced_from

                       [ goal(atom(X)),

                         goal(checktype(X,TYPE)),

                         goal(type(TYPE,enumerated)),

                         goal(enumeration(TYPE,[A,B,C,D])) ].

enum_cases(5):  X=A or X=B or X=C or X=D or X=E may_be_deduced_from

                       [ goal(atom(X)),

                         goal(checktype(X,TYPE)),

                         goal(type(TYPE,enumerated)),

                         goal(enumeration(TYPE,[A,B,C,D,E])) ].

enum_cases(6):  X=A or X=B or X=C or X=D or X=E or X=F may_be_deduced_from

                       [ goal(atom(X)),

                         goal(checktype(X,TYPE)),

                         goal(type(TYPE,enumerated)),

                         goal(enumeration(TYPE,[A,B,C,D,E,F])) ].

enum_cases(7):  X=A or X=B or X=C or X=D or X=E or X=F or X=G

                             may_be_deduced_from

                       [ goal(atom(X)),

                         goal(checktype(X,TYPE)),

                         goal(type(TYPE,enumerated)),

                         goal(enumeration(TYPE,[A,B,C,D,E,F,G])) ].

enum_cases(8):  X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H

                             may_be_deduced_from

                       [ goal(atom(X)),

                         goal(checktype(X,TYPE)),

                         goal(type(TYPE,enumerated)),

                         goal(enumeration(TYPE,[A,B,C,D,E,F,G,H])) ].

enum_cases(9):  X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I

                             may_be_deduced_from

                               [ goal(atom(X)),

                         goal(checktype(X,TYPE)),

                         goal(type(TYPE,enumerated)),

                         goal(enumeration(TYPE,[A,B,C,D,E,F,G,H,I])) ].

enum_cases(10): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I

                             or X=J may_be_deduced_from

                       [ goal(atom(X)),

                         goal(checktype(X,TYPE)),

                         goal(type(TYPE,enumerated)),

                         goal(enumeration(TYPE,[A,B,C,D,E,F,G,H,I,J])) ].

enum_cases(11): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I

                             or X=J or X=K may_be_deduced_from

                       [ goal(atom(X)),

                         goal(checktype(X,TYPE)),

                         goal(type(TYPE,enumerated)),

                         goal(enumeration(TYPE,[A,B,C,D,E,F,G,H,I,J,K])) ].

enum_cases(12): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I

                             or X=J or X=K or X=L may_be_deduced_from

                       [ goal(atom(X)),

                         goal(checktype(X,TYPE)),

                         goal(type(TYPE,enumerated)),

                         goal(enumeration(TYPE,[A,B,C,D,E,F,G,H,I,J,K,L])) ].

enum_cases(13): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or

                X=J or X=K or X=L or X=M may_be_deduced_from

                      [ goal(atom(X)),

                        goal(checktype(X,TYPE)),

                        goal(type(TYPE,enumerated)),

                        goal(enumeration(TYPE,[A,B,C,D,E,F,G,H,I,J,K,L,M])) ].

enum_cases(14): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or

                X=J or X=K or X=L or X=M or X=N may_be_deduced_from

                      [ goal(atom(X)),

                        goal(checktype(X,TYPE)),

                        goal(type(TYPE,enumerated)),

                        goal(enumeration(TYPE,

                                    [A,B,C,D,E,F,G,H,I,J,K,L,M,N])) ].

enum_cases(15): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or

                X=J or X=K or X=L or X=M or X=N or X=O may_be_deduced_from

                       [ goal(atom(X)),

                         goal(checktype(X,TYPE)),

                         goal(type(TYPE,enumerated)),

                         goal(enumeration(TYPE,

                                    [A,B,C,D,E,F,G,H,I,J,K,L,M,N,O])) ].

enum_cases(16): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or

                X=J or X=K or X=L or X=M or X=N or X=O or X=P

                             may_be_deduced_from

                       [ goal(atom(X)),

                         goal(checktype(X,TYPE)),

                         goal(type(TYPE,enumerated)),

                         goal(enumeration(TYPE,

                                    [A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P])) ].

enum_cases(17): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or

                X=J or X=K or X=L or X=M or X=N or X=O or X=P or X=Q

                             may_be_deduced_from

                       [ goal(atom(X)),

                         goal(checktype(X,TYPE)),

                         goal(type(TYPE,enumerated)),

                         goal(enumeration(TYPE,

                                    [A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q])) ].

enum_cases(18): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or

                X=J or X=K or X=L or X=M or X=N or X=O or X=P or X=Q or X=R

                             may_be_deduced_from

                       [ goal(atom(X)),

                         goal(checktype(X,TYPE)),

                         goal(type(TYPE,enumerated)),

                         goal(enumeration(TYPE,

                                    [A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R])) ].

enum_cases(19): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or

                X=J or X=K or X=L or X=M or X=N or X=O or X=P or X=Q or X=R or

                X=S may_be_deduced_from

                       [ goal(atom(X)),

                         goal(checktype(X,TYPE)),

                         goal(type(TYPE,enumerated)),

                         goal(enumeration(TYPE,

                                    [A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S])) ].

enum_cases(20): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or

                X=J or X=K or X=L or X=M or X=N or X=O or X=P or X=Q or X=R or

                X=S or X=T may_be_deduced_from

                       [ goal(atom(X)),

                         goal(checktype(X,TYPE)),

                         goal(type(TYPE,enumerated)),

                         goal(enumeration(TYPE,

                                    [A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T])) ].

enum_cases(21): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or

                X=J or X=K or X=L or X=M or X=N or X=O or X=P or X=Q or X=R or

                X=S or X=T or X=U may_be_deduced_from

                       [ goal(atom(X)),

                         goal(checktype(X,TYPE)),

                         goal(type(TYPE,enumerated)),

                         goal(enumeration(TYPE,

                                    [A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U])) ].

enum_cases(22): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or

                X=J or X=K or X=L or X=M or X=N or X=O or X=P or X=Q or X=R or

                X=S or X=T or X=U or X=V may_be_deduced_from

                       [ goal(atom(X)),

                         goal(checktype(X,TYPE)),

                         goal(type(TYPE,enumerated)),

                         goal(enumeration(TYPE,

                                    [A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V])) ].

enum_cases(23): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or

                X=J or X=K or X=L or X=M or X=N or X=O or X=P or X=Q or X=R or

                X=S or X=T or X=U or X=V or X=W may_be_deduced_from

                       [ goal(atom(X)),

                         goal(checktype(X,TYPE)),

                         goal(type(TYPE,enumerated)),

                         goal(enumeration(TYPE,

                                    [A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W])) ].

enum_cases(24): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or

                X=J or X=K or X=L or X=M or X=N or X=O or X=P or X=Q or X=R or

                X=S or X=T or X=U or X=V or X=W or X=Y may_be_deduced_from

                       [ goal(atom(X)),

                         goal(checktype(X,TYPE)),

                         goal(type(TYPE,enumerated)),

                         goal(enumeration(TYPE,[A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,

                                               P,Q,R,S,T,U,V,W,Y])) ].

enum_cases(25): X=A or X=B or X=C or X=D or X=E or X=F or X=G or X=H or X=I or

                X=J or X=K or X=L or X=M or X=N or X=O or X=P or X=Q or X=R or

                X=S or X=T or X=U or X=V or X=W or X=Y or X=Z

                             may_be_deduced_from

                       [ goal(atom(X)),

                         goal(checktype(X,TYPE)),

                         goal(type(TYPE,enumerated)),

                         goal(enumeration(TYPE,[A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,

                                               P,Q,R,S,T,U,V,W,Y,Z])) ].

4.5               ENUMERATION.RUL

%-------------------------------------------------------------------------------

%  (C) Altran Praxis Limited

%-------------------------------------------------------------------------------

%

%  The SPARK toolset is free software; you can redistribute it and/or modify it

%  under terms of the GNU General Public License as published by the Free

%  Software Foundation; either version 3, or (at your option) any later

%  version. The SPARK toolset is distributed in the hope that it will be

%  useful, but WITHOUT ANY WARRANTY; without even the implied warranty of

%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General

%  Public License for more details. You should have received a copy of the GNU

%  General Public License distributed with the SPARK toolset; see file

%  COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of

%  the license.

%

%===============================================================================

 

 

%-------------------------------------------------------------------------------

% RULE FAMILIES CONTAINED HEREIN :-

%

% enumeration  : more properties of enumerated types (pred & succ etc.)

%-------------------------------------------------------------------------------

% MODEL DECLARATIONS FOR THIS FILE :-

%

% rule_family enumeration:

%         X <= Y  requires [ X:e,   Y:e   ] &

%         X < Y   requires [ X:e,   Y:e   ] &

%         X >= Y  requires [ X:e,   Y:e   ] &

%         X > Y   requires [ X:e,   Y:e   ] &

%         X <> Y  requires [ X:e,   Y:e   ] &

%         succ(X) requires [ X:e          ] &

%         pred(X) requires [ X:e          ].

%-------------------------------------------------------------------------------

/*** Enumerated type inequality rules ***/

 

/* Predecessor */

 

enumeration(1):              X <= pred(Y) may_be_deduced_from [ X < Y        ].

enumeration(2):              pred(X) <= Y may_be_deduced_from

                                    [ X <= Y, goal(checktype(X, T)),

                                      goal(enumeration(T, [E|_])),

                                      X <> E ].

enumeration(3):              pred(X) >= Y may_be_deduced_from [ X > Y        ].

enumeration(4):              X >= pred(Y) may_be_deduced_from

                                    [ X >= Y, goal(checktype(Y, T)),

                                      goal(enumeration(T, [E|_])),

                                      Y <> E ].

 

enumeration(5):              X > Y        may_be_deduced_from [ pred(X) >= Y ].

enumeration(6):              X < Y        may_be_deduced_from [ X <= pred(Y) ].

enumeration(7):              X <= Y       may_be_deduced_from [ pred(X) < Y  ].

enumeration(8):              X >= Y       may_be_deduced_from [ X > pred(Y)  ].

 

enumeration(9):              pred(X) < Y  may_be_deduced_from

                                    [ X <= Y, goal(checktype(X, T)),

                                      goal(enumeration(T, [E|_])),

                                      X <> E ].

enumeration(10):     X > pred(Y)  may_be_deduced_from

                                    [ X >= Y, goal(checktype(Y, T)),

                                      goal(enumeration(T, [E|_])),

                                      Y <> E ].

 

enumeration(11):     pred(X) < X  may_be_deduced_from

                                    [ goal(checktype(X, T)),

                                      goal(enumeration(T,[E|_])),

                                      X <> E ].

enumeration(12):     X > pred(X)  may_be_deduced_from

                                    [ goal(checktype(X, T)),

                                      goal(enumeration(T,[E|_])),

                                      X <> E ].

 

 

/* Successor */

 

enumeration(13):     X <= succ(Y) may_be_deduced_from

                                    [ X <= Y, goal(checktype(Y, T)),

                                      goal(enumeration(T, L)),

                                      goal(last(L, E)),

                                      Y <> E ].

enumeration(14):     succ(X) <= Y may_be_deduced_from [ X < Y        ].

enumeration(15):     succ(X) >= Y may_be_deduced_from

                                    [ X >= Y, goal(checktype(X, T)),

                                      goal(enumeration(T, L)),

                                      goal(last(L, E)),

                                      X <> E ].

enumeration(16):     X >= succ(Y) may_be_deduced_from [ X > Y        ].

 

enumeration(17):     X < Y        may_be_deduced_from [ succ(X) <= Y ].

enumeration(18):     X > Y        may_be_deduced_from [ X >= succ(Y) ].

enumeration(19):     X >= Y       may_be_deduced_from [ succ(X) > Y  ].

enumeration(20):     X <= Y       may_be_deduced_from [ X < succ(Y)  ].

 

enumeration(21):     succ(X) > Y  may_be_deduced_from

                                    [ X >= Y, goal(checktype(X, T)),

                                      goal(enumeration(T, L)),

                                      goal(last(L, E)),

                                      X <> E ].

enumeration(22):     X < succ(Y)  may_be_deduced_from

                                    [ X <= Y, goal(checktype(Y, T)),

                                      goal(enumeration(T, L)),

                                      goal(last(L, E)),

                                      Y <> E ].

 

enumeration(23):     succ(X) > X  may_be_deduced_from

                                    [ goal(checktype(X, T)),

                                      goal(enumeration(T, L)),

                                      goal(last(L, E)),

                                      X <> E ].

enumeration(24):     X < succ(X)  may_be_deduced_from

                                    [ goal(checktype(X, T)),

                                      goal(enumeration(T, L)),

                                      goal(last(L, E)),

                                      X <> E ].

 

 

/* General */

 

enumeration(25):     X <> E       may_be_deduced_from

                                    [ X > Y, goal(checktype(X, T)),

                                      goal(enumeration(T, [E|_])) ].

 

enumeration(26):     X <> E       may_be_deduced_from

                                    [ X < Y, goal(checktype(X, T)),

                                      goal(enumeration(T, L)),

                                      goal(last(L, E)) ].

 

 

/*============================================================================*

 

 Justifications

 --------------

 

 1:  If X < Y, then X <= pred(Y) must hold.  (Note that because X < Y, Y

     cannot be equal to the first enumeration literal in its type.)

 2:  If X <= Y, then if pred(X) exists it must also be <= Y.  (The additional

     immediate conditions ensure X is not the first literal, so pred(X)

     does indeed exist.)

 3:  This rule is equivalent to rule 1 (though with X and Y interchanged).

 4:  This rule is equivalent to rule 2 (though with X and Y interchanged).

 5:  Given pred(X) >= Y, X cannot be the first enumeration literal in its type

     and given X > pred(X) (rule 12) we see X > Y by transitivity.

 6:  This rule is equivalent to rule 5 (though with X and Y interchanged).

 7:  Given pred(X) < Y, X cannot be the first enumeration literal in its type.

     If pred(X) < Y it follows that X <= Y (since if X > Y were to hold, then

     pred(X) would have to be at least Y).

 8:  This rule is equivalent to rule 7 (though with X and Y interchanged).

 9:  If X <= Y then provided X is not equal to the first enumeration literal

     in its type, pred(X) exists and pred(X) < X (rule 11), so pred(X) < Y by

     transitivity.

 10: This rule is equivalent to rule 9 (though with X and Y interchanged).

 11: If X is not equal to the first enumeration literal in its type, then

     pred(X) exists.  Whenever this is so, pred(X) precedes X in the type,

     so pred(X) < X holds in such cases as required.

 12: This rule is equivalent to rule 11.

 13: If Y is not equal to the last enumeration literal in its type, then

     succ(Y) exists and Y<succ(Y) (rule 24), so X <= succ(Y) by transitivity.

 14: If X < Y, X cannot be the last enumeration literal in its type, so

     succ(X) exists and must be at most Y (since if it were greater than Y,

     then X would have to be at least Y, contradicting X < Y).

 15: This rule is equivalent to rule 13 (though with X and Y interchanged).

 16: This rule is equivalent to rule 14 (though with X and Y interchanged).

 17: Given succ(X) <= Y, X is not the last enumeration literal in its type, so

     X < succ(X) (rule 24), thus X < Y by transitivity.

 18: This rule is equivalent to rule 17 (though with X and Y interchanged).

 19: If succ(X) > Y, then X must be at least Y as required.

 20: This rule is equivalent to rule 19 (though with X and Y interchanged).

 21: If X is not the last enumeration literal in its type, then succ(X) > X

     (rule 23), so succ(X) > Y follows from X >= Y by transitivity.

 22: This rule is equivalent to rule 21 (though with X and Y interchanged).

 23: If X is not equal to the last enumeration literal in its type, then

     succ(X) exists.  Whenever this is so, succ(X) succeeds X in the type,

     so succ(X) > X holds in such cases as required.

 24: This rule is equivalent to rule 23.

 25: If X is bigger than something (Y), then X cannot be equal to the first

     enumeration literal in its type.

 26: If X is smaller than something (Y), then X cannot be equal to the last

     enumeration literal in its type.

 

*============================================================================*/


4.6               FDLFUNCS.RUL

%-------------------------------------------------------------------------------

%  (C) Altran Praxis Limited

%-------------------------------------------------------------------------------

%

%  The SPARK toolset is free software; you can redistribute it and/or modify it

%  under terms of the GNU General Public License as published by the Free

%  Software Foundation; either version 3, or (at your option) any later

%  version. The SPARK toolset is distributed in the hope that it will be

%  useful, but WITHOUT ANY WARRANTY; without even the implied warranty of

%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General

%  Public License for more details. You should have received a copy of the GNU

%  General Public License distributed with the SPARK toolset; see file

%  COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of

%  the license.

%

%===============================================================================

 

 

%-------------------------------------------------------------------------------

% RULE FAMILIES CONTAINED HEREIN :-

%

% abs          : properties of the absolute value function abs(_)

% sqr          : properties of the square function sqr(_)

% odd          : properties of predicate odd(_)

% exp          : properties of the exponentiation operator **

%-------------------------------------------------------------------------------

% MODEL DECLARATIONS FOR THIS FILE :-

%

% rule_family abs:

%         abs(X) requires [ X:ir         ] &

%         X >= Y requires [ X:ir,  Y:ir  ] &

%         X > Y  requires [ X:ir,  Y:ir  ] &

%         X or Y requires [ X:any, Y:any ] &

%         X * Y  requires [ X:ir,  Y:ir  ].

%

% rule_family sqr:

%         sqr(X) requires [ X:ir       ] &

%         X >= Y requires [ X:ir, Y:ir ] &

%         X > Y  requires [ X:ir, Y:ir ] &

%         X * Y  requires [ X:ir, Y:ir ] &

%         abs(X) requires [ X:ir       ].

%

% rule_family odd:

%         odd(X) requires [ X:i        ] &

%         not X  requires [ X:any      ] &

%         X <> Y requires [ X:i,   Y:i ] &

%         X = Y  requires [ X:i,   Y:i ].

%

% rule_family exp:

%         X ** Y requires [ X:ir, Y:i  ] &

%         X * Y  requires [ X:ir, Y:ir ] &

%         X >= Y requires [ X:ir, Y:ir ] &

%         X <= Y requires [ X:ir, Y:ir ] &

%         X > Y  requires [ X:ir, Y:ir ] &

%         X < Y  requires [ X:ir, Y:ir ].

%-------------------------------------------------------------------------------

/*** ABS:  absolute value function properties ***/

 

abs(1): abs(X)      may_be_replaced_by X if [ X>=0 ].

abs(2): abs(X)      may_be_replaced_by -X if [ X<=0 ].

abs(3): abs(X)>=0   may_be_deduced.

abs(4): abs(X)>0    may_be_deduced_from [ X<>0 ].

abs(5): abs(X)=X or abs(X)=(-X) may_be_deduced.

abs(6): abs(abs(X)) may_be_replaced_by abs(X).

abs(7): abs(X*Y) & abs(X)*abs(Y) are_interchangeable.

 

 

/*** SQR:  square function properties ***/

 

sqr(1): sqr(X)      may_be_replaced_by X*X.

sqr(2): sqr(X)>=0   may_be_deduced.

sqr(3): sqr(X)>0    may_be_deduced_from [ X<>0 ].

sqr(4): sqr(X*Y) & sqr(X)*sqr(Y) are_interchangeable.

sqr(5): abs(sqr(X)) may_be_replaced_by sqr(X).

sqr(6): sqr(abs(X)) may_be_replaced_by sqr(X).

 

 

/*** ODD:  odd function properties ***/

 

odd(1): odd(X)     & (X div 2) * 2 <> X are_interchangeable.

odd(2): not odd(X) & (X div 2) * 2 =  X are_interchangeable.

 

odd(3): odd(X)           may_be_deduced_from [ X=2*K+1 ].

odd(4): not odd(X)       may_be_deduced_from [ X=2*K ].

 

odd(5): odd(X)           may_be_deduced_from [ odd(-X) ].

odd(6): odd(-X)          may_be_deduced_from [ odd(X) ].

odd(7): not odd(X)       may_be_deduced_from [ not odd(-X) ].

odd(8): not odd(-X)      may_be_deduced_from [ not odd(X) ].

 

odd(9): odd(X+Y)         may_be_deduced_from [ odd(X), not odd(Y) ].

odd(10): odd(X+Y)        may_be_deduced_from [ not odd(X), odd(Y) ].

odd(11): not odd(X+Y)    may_be_deduced_from [ not odd(X), not odd(Y) ].

odd(12): not odd(X+Y)    may_be_deduced_from [ odd(X), odd(Y) ].

 

odd(13): odd(X-Y)        may_be_deduced_from [ odd(X), not odd(Y) ].

odd(14): odd(X-Y)        may_be_deduced_from [ not odd(X), odd(Y) ].

odd(15): not odd(X-Y)    may_be_deduced_from [ not odd(X), not odd(Y) ].

odd(16): not odd(X-Y)    may_be_deduced_from [ odd(X), odd(Y) ].

 

odd(17): odd(X*Y)        may_be_deduced_from [ odd(X), odd(Y) ].

odd(18): not odd(X*Y)    may_be_deduced_from [ not odd(X) ].

odd(19): not odd(X*Y)    may_be_deduced_from [ not odd(Y) ].

 

odd(20): odd(sqr(X))     may_be_deduced_from [ odd(X) ].

odd(21): odd(X)          may_be_deduced_from [ odd(sqr(X)) ].

odd(22): not odd(sqr(X)) may_be_deduced_from [ not odd(X) ].

odd(23): not odd(X)      may_be_deduced_from [ not odd(sqr(X)) ].

 

odd(24): odd(abs(X))     may_be_deduced_from [ odd(X) ].

odd(25): odd(X)          may_be_deduced_from [ odd(abs(X)) ].

odd(26): not odd(abs(X)) may_be_deduced_from [ not odd(X) ].

odd(27): not odd(X)      may_be_deduced_from [ not odd(abs(X)) ].

 

 

/*** EXP: exponentiation operator properties - for non-negative exponents ***/

 

exp(1):  X**0     may_be_replaced_by 1.

exp(2):  0**Y     may_be_replaced_by 0               if [ Y>=1 ].

exp(3):  1**Y     may_be_replaced_by 1               if [ Y>=0 ].

 

exp(4):  X**Y     & X*(X**(Y-1)) are_interchangeable if [ Y>0 ].

exp(5):  X**(Y+1) & X*(X**Y)     are_interchangeable if [ Y>=0 ].

 

exp(6):  (-X)**Y  may_be_replaced_by X**Y            if [ not odd(Y) ].

exp(7):  (-X)**Y  may_be_replaced_by -(X**Y)         if [ odd(Y) ].

 

exp(8):  X**1     may_be_replaced_by X.

exp(9):  X**2     may_be_replaced_by X*X.

exp(10): X**3     may_be_replaced_by X*X*X.

exp(11): X**4     may_be_replaced_by X*X*X*X.

 

exp(12): X**Y>=0  may_be_deduced_from [ X>=0, Y>=0 ].

exp(13): X**Y>=0  may_be_deduced_from [ not odd(Y) ].

 

exp(14): X**Y<=0  may_be_deduced_from [ X<=0, odd(Y) ].

 

exp(15): X**Y>0   may_be_deduced_from [ X>0 ].

exp(16): X**Y>0   may_be_deduced_from [ X<0, not odd(Y) ].

 

exp(17): X**Y<0   may_be_deduced_from [ X<0, odd(Y) ].


4.7               GENINEQS.RUL

%-------------------------------------------------------------------------------

%  (C) Altran Praxis Limited

%-------------------------------------------------------------------------------

%

%  The SPARK toolset is free software; you can redistribute it and/or modify it

%  under terms of the GNU General Public License as published by the Free

%  Software Foundation; either version 3, or (at your option) any later

%  version. The SPARK toolset is distributed in the hope that it will be

%  useful, but WITHOUT ANY WARRANTY; without even the implied warranty of

%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General

%  Public License for more details. You should have received a copy of the GNU

%  General Public License distributed with the SPARK toolset; see file

%  COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of

%  the license.

%

%===============================================================================

 

 

%-------------------------------------------------------------------------------

% RULE FAMILIES CONTAINED HEREIN :-

%

% transitivity : transitivity of relational operators

% strengthen   : inequalities strengthening rules

% negation     : negation of inequalities rules

%-------------------------------------------------------------------------------

% MODEL DECLARATIONS FOR THIS FILE :-

%

% rule_family transitivity:

%         X <= Y requires [ X:ire, Y:ire ] &

%         X >= Y requires [ X:ire, Y:ire ] &

%         X < Y  requires [ X:ire, Y:ire ] &

%         X > Y  requires [ X:ire, Y:ire ] &

%         X = Y  requires [ X:any, Y:any ] &

%         X <> Y requires [ X:any, Y:any ].

%

% rule_family strengthen:

%         X > Y  requires [ X:ire, Y:ire ] &

%         X < Y  requires [ X:ire, Y:ire ] &

%         X = Y  requires [ X:ire, Y:ire ].

%

% rule_family negation:

%         not X  requires [ X:any        ] &

%         X <> Y requires [ X:any, Y:any ] &

%         X = Y  requires [ X:any, Y:any ] &

%         X <= Y requires [ X:ire, Y:ire ] &

%         X > Y  requires [ X:ire, Y:ire ] &

%         X >= Y requires [ X:ire, Y:ire ] &

%         X < Y  requires [ X:ire, Y:ire ].

%-------------------------------------------------------------------------------

/*** TRANSITIVITY Rules ***/

 

transitivity(1):        I<=K may_be_deduced_from [ I<=J, J<=K ].

transitivity(2):        I<=K may_be_deduced_from [ I<=J, J<K  ].

transitivity(3):        I<=K may_be_deduced_from [ I<=J, J=K  ].

transitivity(4):        I<=K may_be_deduced_from [ I<J,  J<=K ].

transitivity(5):        I<=K may_be_deduced_from [ I<J,  J<K  ].

transitivity(6):        I<=K may_be_deduced_from [ I<J,  J=K  ].

transitivity(7):        I<=K may_be_deduced_from [ I=J,  J<=K ].

transitivity(8):        I<=K may_be_deduced_from [ I=J,  J<K  ].

transitivity(9):        I<=K may_be_deduced_from [ I=J,  J=K  ].

transitivity(10):       K>=I may_be_deduced_from [ I<=J, J<=K ].

transitivity(11):       K>=I may_be_deduced_from [ I<=J, J<K  ].

transitivity(12):       K>=I may_be_deduced_from [ I<=J, J=K  ].

transitivity(13):       K>=I may_be_deduced_from [ I<J,  J<=K ].

transitivity(14):       K>=I may_be_deduced_from [ I<J,  J<K  ].

transitivity(15):       K>=I may_be_deduced_from [ I<J,  J=K  ].

transitivity(16):       K>=I may_be_deduced_from [ I=J,  J<=K ].

transitivity(17):       K>=I may_be_deduced_from [ I=J,  J<K  ].

transitivity(18):       K>=I may_be_deduced_from [ I=J,  J=K  ].

transitivity(19):       I<K  may_be_deduced_from [ I<=J, J<K  ].

transitivity(20):       I<K  may_be_deduced_from [ I<J,  J<=K ].

transitivity(21):       I<K  may_be_deduced_from [ I<J,  J<K  ].

transitivity(22):       I<K  may_be_deduced_from [ I<J,  J=K  ].

transitivity(23):       I<K  may_be_deduced_from [ I=J,  J<K  ].

transitivity(24):       K>I  may_be_deduced_from [ I<=J, J<K  ].

transitivity(25):       K>I  may_be_deduced_from [ I<J,  J<=K ].

transitivity(26):       K>I  may_be_deduced_from [ I<J,  J<K  ].

transitivity(27):       K>I  may_be_deduced_from [ I<J,  J=K  ].

transitivity(28):       K>I  may_be_deduced_from [ I=J,  J<K  ].

transitivity(29):       I=K  may_be_deduced_from [ I=J,  J=K  ].

transitivity(30):       I<>K may_be_deduced_from [ I<>J, J=K  ].

 

 

 

/*** STRENGTHEN Rules ***/

 

strengthen(1):  I>J may_be_deduced_from [ I>=J, I<>J ].

strengthen(2):  J<I may_be_deduced_from [ I>=J, I<>J ].

strengthen(3):  I=J may_be_deduced_from [ I>=J, I<=J ].

 

 

 

/*** Rules for manipulation of logical NOT operator ***/

 

negation(1):    not(A=B) & A<>B are_interchangeable.

negation(2):    not(A<>B) & A=B are_interchangeable.

negation(3):    not(A>B) & A<=B are_interchangeable.

negation(4):    not(A<=B) & A>B are_interchangeable.

negation(5):    not(A<B) & A>=B are_interchangeable.

negation(6):    not(A>=B) & A<B are_interchangeable.

negation(7):    not(A=B) & B<>A are_interchangeable.

negation(8):    not(A<>B) & B=A are_interchangeable.

negation(9):    not(A>B) & B>=A are_interchangeable.

negation(10):   not(A<=B) & B<A are_interchangeable.

negation(11):   not(A<B) & B<=A are_interchangeable.

negation(12):   not(A>=B) & B>A are_interchangeable.

 

4.8               INTINEQS.RUL

%-------------------------------------------------------------------------------

%  (C) Altran Praxis Limited

%-------------------------------------------------------------------------------

%

%  The SPARK toolset is free software; you can redistribute it and/or modify it

%  under terms of the GNU General Public License as published by the Free

%  Software Foundation; either version 3, or (at your option) any later

%  version. The SPARK toolset is distributed in the hope that it will be

%  useful, but WITHOUT ANY WARRANTY; without even the implied warranty of

%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General

%  Public License for more details. You should have received a copy of the GNU

%  General Public License distributed with the SPARK toolset; see file

%  COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of

%  the license.

%

%===============================================================================

 

 

%-------------------------------------------------------------------------------

% RULE FAMILY CONTAINED HEREIN :-

%

% inequals     : inequalities rules applicable to integers only

%-------------------------------------------------------------------------------

% MODEL DECLARATION FOR THIS FILE :-

%

% rule_family inequals:

%         X >= Y requires [ X:i, Y:i ] &

%         X <= Y requires [ X:i, Y:i ] &

%         X > Y  requires [ X:i, Y:i ] &

%         X = Y  requires [ X:i, Y:i ].

%-------------------------------------------------------------------------------

/*** Integer division basic properties ***/

 

inequals(86):   N*(A div N)>=A-N+1 may_be_deduced_from [ N>0, A>=0 ].

inequals(87):   (A div N)*N>=A-N+1 may_be_deduced_from [ N>0, A>=0 ].

inequals(88):   N*(A div N)<=A may_be_deduced_from [ N<>0, A>=0 ].

inequals(89):   (A div N)*N<=A may_be_deduced_from [ N<>0, A>=0 ].

inequals(90):   A div N>=0 may_be_deduced_from [ A>=0, N>0 ].

inequals(91):   A div N>0  may_be_deduced_from [ A>=N, N>0 ].

inequals(92):   A div N>0  may_be_deduced_from [ A<=N, N<0 ].

inequals(93):   I div N<=J div N may_be_deduced_from [ I<=J, N>0 ].

inequals(94):   I div N>=J div N may_be_deduced_from [ I>=J, N>0 ].

inequals(95):   I div M=J div N  may_be_deduced_from [ I=J, M=N ].

inequals(96):   N*(A div N)>=A+N+1 may_be_deduced_from [ N<0, A>=0 ].

inequals(97):   (A div N)*N>=A+N+1 may_be_deduced_from [ N<0, A>=0 ].

inequals(98):   A div B>=0 may_be_deduced_from [ A<=0, B<0 ].

inequals(99):   A div B<=0 may_be_deduced_from [ A>=0, B<0 ].

inequals(100):  A div B<=0 may_be_deduced_from [ A<=0, B>0 ].

 

/*** Other useful integers-only rules ***/

 

inequals(101):  X>=Y+1 may_be_deduced_from [ X>Y ].

inequals(102):  Y+1<=X may_be_deduced_from [ X>Y ].

inequals(103):  X>=1   may_be_deduced_from [ X>0 ].

4.9               NUMINEQS.RUL

%-------------------------------------------------------------------------------

%  (C) Altran Praxis Limited

%-------------------------------------------------------------------------------

%

%  The SPARK toolset is free software; you can redistribute it and/or modify it

%  under terms of the GNU General Public License as published by the Free

%  Software Foundation; either version 3, or (at your option) any later

%  version. The SPARK toolset is distributed in the hope that it will be

%  useful, but WITHOUT ANY WARRANTY; without even the implied warranty of

%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General

%  Public License for more details. You should have received a copy of the GNU

%  General Public License distributed with the SPARK toolset; see file

%  COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of

%  the license.

%

%===============================================================================

 

 

%-------------------------------------------------------------------------------

% RULE FAMILIES CONTAINED HEREIN :-

%

% inequals     : inequalities rules for integers and reals

% zero         : equality/non-equality to 0 with multiplication rules

%-------------------------------------------------------------------------------

% MODEL DECLARATIONS FOR THIS FILE :-

%

% rule_family inequals:

%         X < Y  requires [ X:ir, Y:ir ] &

%         X <= Y requires [ X:ir, Y:ir ] &

%         X > Y  requires [ X:ir, Y:ir ] &

%         X >= Y requires [ X:ir, Y:ir ] &

%         X <> Y requires [ X:ir, Y:ir ] &

%         X = Y  requires [ X:ir, Y:ir ].

%

% rule_family zero:

%         X = Y  requires [ X:ir,  Y:ir  ] &

%         X <> Y requires [ X:ir,  Y:ir  ] &

%         X or Y requires [ X:any, Y:any ].

%-------------------------------------------------------------------------------

 

/*** INEQUALS Rules ***/

 

/*** Addition or subtraction of a number from one side of an inequality ***/

 

inequals(1):    I-N<J may_be_deduced_from [ I<J, N>=0 ].

inequals(2):    I-N<J may_be_deduced_from [ I<=J, N>0 ].

inequals(3):    I-N<=J may_be_deduced_from [ I<=J, N>=0 ].

 

inequals(4):    J>I-N may_be_deduced_from [ I<J, N>=0 ].

inequals(5):    J>I-N may_be_deduced_from [ I<=J, N>0 ].

inequals(6):    J>=I-N may_be_deduced_from [ I<=J, N>=0 ].

 

inequals(7):    I+N>J may_be_deduced_from [ I>J, N>=0 ].

inequals(8):    I+N>J may_be_deduced_from [ I>=J, N>0 ].

inequals(9):    I+N>=J may_be_deduced_from [ I>=J, N>=0 ].

 

inequals(10):   N+I>J may_be_deduced_from [ I>J, N>=0 ].

inequals(11):   N+I>J may_be_deduced_from [ I>=J, N>0 ].

inequals(12):   N+I>=J may_be_deduced_from [ I>=J, N>=0 ].

 

inequals(13):   J<I+N may_be_deduced_from [ I>J, N>=0 ].

inequals(14):   J<I+N may_be_deduced_from [ I>=J, N>0 ].

inequals(15):   J<=I+N may_be_deduced_from [ I>=J, N>=0 ].

 

inequals(16):   J<N+I may_be_deduced_from [ I>J, N>=0 ].

inequals(17):   J<N+I may_be_deduced_from [ I>=J, N>0 ].

inequals(18):   J<=N+I may_be_deduced_from [ I>=J, N>=0 ].

 

 

/*** Addition and subtraction of a number on both sides of an inequality ***/

 

inequals(19):   I+N<J+N may_be_deduced_from [ I<J ].

inequals(20):   N+I<J+N may_be_deduced_from [ I<J ].

inequals(21):   I+N<N+J may_be_deduced_from [ I<J ].

inequals(22):   N+I<N+J may_be_deduced_from [ I<J ].

 

inequals(23):   I+N>J+N may_be_deduced_from [ I>J ].

inequals(24):   N+I>J+N may_be_deduced_from [ I>J ].

inequals(25):   I+N>N+J may_be_deduced_from [ I>J ].

inequals(26):   N+I>N+J may_be_deduced_from [ I>J ].

 

inequals(27):   I+N<>J+N may_be_deduced_from [ I<>J ].

inequals(28):   N+I<>J+N may_be_deduced_from [ I<>J ].

inequals(29):   I+N<>N+J may_be_deduced_from [ I<>J ].

inequals(30):   N+I<>N+J may_be_deduced_from [ I<>J ].

 

inequals(31):   I-N<J-N may_be_deduced_from [ I<J ].

inequals(32):   I-N>J-N may_be_deduced_from [ I>J ].

inequals(33):   I-N<>J-N may_be_deduced_from [ I<>J ].

 

 

/*** Multiplication on both sides of an inequality by a number ***/

 

inequals(34):   I*N<>J*N may_be_deduced_from [ I<>J, N<>0 ].

inequals(35):   I*N>J*N may_be_deduced_from [ I>J, N>0 ].

inequals(36):   I*N<J*N may_be_deduced_from [ I<J, N>0 ].

inequals(37):   I*N>J*N may_be_deduced_from [ I<J, N<0 ].

inequals(38):   I*N<J*N may_be_deduced_from [ I>J, N<0 ].

inequals(39):   I*N>=J*N may_be_deduced_from [ I>=J, N>=0 ].

inequals(40):   I*N<=J*N may_be_deduced_from [ I<=J, N>=0 ].

inequals(41):   I*N>=J*N may_be_deduced_from [ I<=J, N<=0 ].

inequals(42):   I*N<=J*N may_be_deduced_from [ I>=J, N<=0 ].

 

 

/*** Addition and subtraction of two inequalities ***/

 

inequals(43):   A+C>B+D may_be_deduced_from [ A>=B, C>D ].

inequals(44):   A+C>B+D may_be_deduced_from [ A>B, C>=D ].

inequals(45):   A+C>B+D may_be_deduced_from [ A>=D, C>B ].

inequals(46):   A+C>B+D may_be_deduced_from [ A>D, C>=B ].

inequals(47):   A-D>B-C may_be_deduced_from [ A>=B, C>D ].

inequals(48):   A-D>B-C may_be_deduced_from [ A>B, C>=D ].

 

inequals(49):   A+C<B+D may_be_deduced_from [ A<=B, C<D ].

inequals(50):   A+C<B+D may_be_deduced_from [ A<B, C<=D ].

inequals(51):   A+C<B+D may_be_deduced_from [ A<=D, C<B ].

inequals(52):   A+C<B+D may_be_deduced_from [ A<D, C<=B ].

inequals(53):   A-D<B-C may_be_deduced_from [ A<=B, C<D ].

inequals(54):   A-D<B-C may_be_deduced_from [ A<B, C<=D ].

 

inequals(55):   A+C<>B+D may_be_deduced_from [ A<>B, C=D ].

inequals(56):   A+C<>B+D may_be_deduced_from [ A=B, C<>D ].

inequals(57):   A+C<>B+D may_be_deduced_from [ A<>D, B=C ].

inequals(58):   A+C<>B+D may_be_deduced_from [ A=D, B<>C ].

inequals(59):   A-D<>B-C may_be_deduced_from [ A<>B, C=D ].

inequals(60):   A-D<>B-C may_be_deduced_from [ A=B, C<>D ].

 

 

/*** Addition and subtraction of a number on both sides of an inequality ***/

 

inequals(61):   I+N=J+N may_be_deduced_from [ I=J ].

inequals(62):   N+I=J+N may_be_deduced_from [ I=J ].

inequals(63):   I+N=N+J may_be_deduced_from [ I=J ].

inequals(64):   N+I=N+J may_be_deduced_from [ I=J ].

 

inequals(65):   I+N<=J+N may_be_deduced_from [ I<=J ].

inequals(66):   N+I<=J+N may_be_deduced_from [ I<=J ].

inequals(67):   I+N<=N+J may_be_deduced_from [ I<=J ].

inequals(68):   N+I<=N+J may_be_deduced_from [ I<=J ].

 

inequals(69):   I+N>=J+N may_be_deduced_from [ I>=J ].

inequals(70):   N+I>=J+N may_be_deduced_from [ I>=J ].

inequals(71):   I+N>=N+J may_be_deduced_from [ I>=J ].

inequals(72):   N+I>=N+J may_be_deduced_from [ I>=J ].

 

inequals(73):   I-N=J-N may_be_deduced_from [ I=J ].

inequals(74):   I-N<=J-N may_be_deduced_from [ I<=J ].

inequals(75):   I-N>=J-N may_be_deduced_from [ I>=J ].

 

/*** Multiplication on both sides of an inequality by a number ***/

 

inequals(76):   I*N=J*N may_be_deduced_from [ I=J ].

 

 

/*** Addition and subtraction of two inequalities ***/

 

inequals(77):   A+C>=B+D may_be_deduced_from [ A>=B, C>=D ].

inequals(78):   A+C>=B+D may_be_deduced_from [ A>=D, C>=B ].

inequals(79):   A-D>=B-C may_be_deduced_from [ A>=B, C>=D ].

 

inequals(80):   A+C<=B+D may_be_deduced_from [ A<=B, C<=D ].

inequals(81):   A+C<=B+D may_be_deduced_from [ A<=D, C<=B ].

inequals(82):   A-D<=B-C may_be_deduced_from [ A<=B, C<=D ].

 

inequals(83):   A+C=B+D may_be_deduced_from [ A=B, C=D ].

inequals(84):   A+C=B+D may_be_deduced_from [ A=D, B=C ].

inequals(85):   A-D=B-C may_be_deduced_from [ A=B, C=D ].

 

 

/* Rule numbering gap: 86-103 are in INTINEQS; retained for compatibility */

 

 

/*** Additional rules for inequalities with multiplication ***/

 

inequals(104):  X=Y     may_be_deduced_from [ X*N=Y*N, N<>0 ].

 

inequals(105):  X<>Y    may_be_deduced_from [ X*N<>Y*N, N<>0 ].

 

inequals(106):  X<=Y    may_be_deduced_from [ X*N<=Y*N, N>0 ].

inequals(107):  X<=Y    may_be_deduced_from [ X*N>=Y*N, N<0 ].

 

inequals(108):  X>=Y    may_be_deduced_from [ X*N>=Y*N, N>0 ].

inequals(109):  X>=Y    may_be_deduced_from [ X*N<=Y*N, N<0 ].

 

inequals(110):  X<Y     may_be_deduced_from [ X*N<Y*N, N>0 ].

inequals(111):  X<Y     may_be_deduced_from [ X*N>Y*N, N<0 ].

 

inequals(112):  X>Y     may_be_deduced_from [ X*N>Y*N, N>0 ].

inequals(113):  X>Y     may_be_deduced_from [ X*N<Y*N, N<0 ].

 

inequals(114):  X*Y<=0  may_be_deduced_from [ X>=0, Y<=0 ].

inequals(115):  X*Y<=0  may_be_deduced_from [ X<=0, Y>=0 ].

 

inequals(116):  X*Y>=0  may_be_deduced_from [ X>=0, Y>=0 ].

inequals(117):  X*Y>=0  may_be_deduced_from [ X<=0, Y<=0 ].

 

inequals(118):  X*Y<0   may_be_deduced_from [ X>0, Y<0 ].

inequals(119):  X*Y<0   may_be_deduced_from [ X<0, Y>0 ].

inequals(120):  X*Y>0   may_be_deduced_from [ X>0, Y>0 ].

inequals(121):  X*Y>0   may_be_deduced_from [ X<0, Y<0 ].

 

 

/*** Rules for equality and non-equality to zero involving multiplication ***/

 

zero(1):        X * Y = 0  may_be_deduced_from [ X = 0 ].

zero(2):        X * Y = 0  may_be_deduced_from [ Y = 0 ].

zero(3):        X=0 or Y=0 may_be_deduced_from [ X*Y=0 ].

zero(4):        X * Y <> 0 may_be_deduced_from [ X<>0, Y<>0 ].

zero(5):        X <> 0     may_be_deduced_from [ X * Y <> 0 ].

zero(6):        Y <> 0     may_be_deduced_from [ X * Y <> 0 ].


4.10          LOGIC.RUL

%-------------------------------------------------------------------------------

%  (C) Altran Praxis Limited

%-------------------------------------------------------------------------------

%

%  The SPARK toolset is free software; you can redistribute it and/or modify it

%  under terms of the GNU General Public License as published by the Free

%  Software Foundation; either version 3, or (at your option) any later

%  version. The SPARK toolset is distributed in the hope that it will be

%  useful, but WITHOUT ANY WARRANTY; without even the implied warranty of

%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General

%  Public License for more details. You should have received a copy of the GNU

%  General Public License distributed with the SPARK toolset; see file

%  COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of

%  the license.

%

%===============================================================================

 

%-------------------------------------------------------------------------------

% RULE FAMILIES CONTAINED HEREIN :-

%

% assoc        : associativity of "and", "or" & "<->"

% commut       : commutativity of "and", "or" & "<->"

% distrib      : distributivity of "and" over "or" and vice versa

% equivalence  : simplification of logical "<->" expressions

% implies      : simplification of logical "->" expressions

% logical      : general logical simplification rules

% logical_and  : simplification of logical "and" expressions

% logical_not  : simplification of logical "not" expressions

% logical_or   : simplification of logical "or" expressions

%-------------------------------------------------------------------------------

% MODEL DECLARATIONS FOR THIS FILE :-

%

% rule_family assoc:

%         X and Y requires [ X:any, Y:any ] &

%         X or Y  requires [ X:any, Y:any ] &

%         X <-> Y requires [ X:any, Y:any ].

%

% rule_family commut:

%         X and Y requires [ X:any, Y:any ] &

%         X or Y  requires [ X:any, Y:any ] &

%         X <-> Y requires [ X:any, Y:any ].

%

% rule_family distrib:

%         X and Y requires [ X:any, Y:any ] &

%         X or Y  requires [ X:any, Y:any ].

%

% rule_family equivalence:

%         X <-> Y requires [ X:any, Y:any ].

%

% rule_family implies:

%         X -> Y requires  [ X:any, Y:any ].

%

% rule_family logical_and:

%         X and Y requires [ X:any, Y:any ].

%

% rule_family logical_not:

%         not X   requires [ X:any ].

%

% rule_family logical_or:

%         X or Y  requires [ X:any, Y:any ].

%

% rule_family logical:

%         not X   requires [ X:any ]        &

%         X and Y requires [ X:any, Y:any ] &

%         X or Y  requires [ X:any, Y:any ] &

%         X -> Y  requires [ X:any, Y:any ] &

%         X <-> Y requires [ X:any, Y:any ].

%-------------------------------------------------------------------------------

 

/*** SIMPLIFICATION OF LOGICAL EXPRESSIONS Rules ***/

 

/*** Simplification of logical “not” expressions ***/

 

logical_not(1):   not true      may_be_replaced_by   false.

logical_not(2):   not false     may_be_replaced_by   true.

logical_not(3):   not not A     may_be_replaced_by   A.

 

 

/*** Simplification of logical “and” expressions ***/

 

logical_and(1):   A and true    may_be_replaced_by   A.

logical_and(2):   true and A    may_be_replaced_by   A.

logical_and(3):   A and false   may_be_replaced_by   false.

logical_and(4):   false and A   may_be_replaced_by   false.

logical_and(5):   A and A       may_be_replaced_by   A.

logical_and(6):   A and not A   may_be_replaced_by   false.

logical_and(7):   (not A) and A may_be_replaced_by   false.

 

 

/*** Simplification of logical “or” expressions ***/

 

logical_or(1):    A or false    may_be_replaced_by   A.

logical_or(2):    false or A    may_be_replaced_by   A.

logical_or(3):    A or true     may_be_replaced_by   true.

logical_or(4):    true or A     may_be_replaced_by   true.

logical_or(5):    A or A        may_be_replaced_by   A.

logical_or(6):    A or not A    may_be_replaced_by   true.

logical_or(7):    (not A) or A  may_be_replaced_by   true.

 

 

/*** Simplification of logical “->” expressions ***/

 

implies(1):       A -> true     may_be_replaced_by   true.

implies(2):       A -> false    may_be_replaced_by   not A.

implies(3):       true -> A     may_be_replaced_by   A.

implies(4):       false -> A    may_be_replaced_by   true.

implies(5):       A -> A        may_be_replaced_by   true.

implies(6):       A -> not A    may_be_replaced_by   not A.

implies(7):       (not A) -> A  may_be_replaced_by   A.

 

 

/*** Simplification of logical “<->” expressions ***/

 

equivalence(1):   A <-> true    may_be_replaced_by   A.

equivalence(2):   true <-> A    may_be_replaced_by   A.

equivalence(3):   A <-> false   may_be_replaced_by   not A.

equivalence(4):   false <-> A   may_be_replaced_by   not A.

equivalence(5):   A <-> A       may_be_replaced_by   true.

equivalence(6):   A <-> not A   may_be_replaced_by   false.

equivalence(7):   (not A) <-> A may_be_replaced_by   false.

 

 

/*** ASSOCIATIVITY of “and”, “or” & “<->” Rules ***/

 

assoc(5):       A and (B and C) & (A and B) and C are_interchangeable.

assoc(6):       A or (B or C)   & (A or B) or C   are_interchangeable.

assoc(7):       A <-> (B <-> C) & (A <-> B) <-> C are_interchangeable.

 

/*** COMMUTATIVITY of “and”, “or” & “<->” Rules ***/

 

commut(3):      A and B         may_be_replaced_by B and A.

commut(4):      A or B          may_be_replaced_by B or A.

commut(5):      A <-> B         may_be_replaced_by B <-> A.

 

/*** DISTRIBUTIVITY of “and” and “or” over each other Rules ***/

 

distrib(5):     (A and B) or C   &  

                             (A or C) and (B or C)  are_interchangeable.

distrib(6):     (A and B) or C   &  

                             (C or A) and (C or B)  are_interchangeable.

distrib(7):     C or (A and B)   &  

                             (C or A) and (C or B)  are_interchangeable.      

distrib(8):     C or (A and B)   &  

                             (A or C) and (B or C)  are_interchangeable.

distrib(9):     (A or B) and C   &  

                             (A and C) or (B and C) are_interchangeable.

distrib(10):    (A or B) and C   &  

                             (C and A) or (C and B) are_interchangeable.

distrib(11):    C and (A or B)   &  

                             (C and A) or (C and B) are_interchangeable.

distrib(12):    C and (A or B)   &  

                             (A and C) or (B and C) are_interchangeable.

 

/*** Other handy logical equivalences (DeMorgan, etc.) ***/

 

logical(1):     not (A or B)     &  

                             (not A) and (not B)    are_interchangeable.

logical(2):     not (A and B)    &  

                             (not A) or (not B)     are_interchangeable.

logical(3):     A -> B           &  

                             (not A) or B           are_interchangeable.

logical(4):     A <-> B          &  

                             (A -> B) and (B -> A)  are_interchangeable.

logical(5):     A -> (B -> C)   

                             may_be_replaced_by         (A and B) -> C.


4.11          MODULAR.RUL

%-------------------------------------------------------------------------------

%  (C) Altran Praxis Limited

%-------------------------------------------------------------------------------

%

%  The SPARK toolset is free software; you can redistribute it and/or modify it

%  under terms of the GNU General Public License as published by the Free

%  Software Foundation; either version 3, or (at your option) any later

%  version. The SPARK toolset is distributed in the hope that it will be

%  useful, but WITHOUT ANY WARRANTY; without even the implied warranty of

%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General

%  Public License for more details. You should have received a copy of the GNU

%  General Public License distributed with the SPARK toolset; see file

%  COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of

%  the license.

%

%===============================================================================

 

%-------------------------------------------------------------------------------

% RULE FAMILIES CONTAINED HEREIN :-

%

% modular : modular arithmetic

%-------------------------------------------------------------------------------

% MODEL DECLARATIONS FOR THIS FILE :-

%

% rule_family modular:

%         X mod Y requires [X : i, Y : i] &

%         X <= Y  requires [X : i, Y : i] &

%         X <> Y  requires [X : i, Y : i] &

%         X < Y   requires [X : i, Y : i] &

%         X = Y   requires [X : i, Y : i].

%-------------------------------------------------------------------------------

/*** Definition of mod (modulo) ***/

 

modular(1):  X mod Y = X - N * Y may_be_deduced_from

                                          [ N * Y <= X, X < (N + 1)* Y,  0 < Y ].

modular(2):  X mod Y = X - N * Y may_be_deduced_from

                                          [ X <= N * Y, (N + 1) * Y < X, Y < 0 ].

 

/*** Bounds for 0 < Y ***/

modular(10):   0 <= (X * Y + Z) mod Y may_be_deduced_from [ 0 <= Z, Z < Y ].

modular(11):   (X * Y + Z) mod Y < Y  may_be_deduced_from [ 0 <= Z, Z < Y ].

 

/*** Bounds for Y < 0 ***/

modular(20):   Y < (X * Y + Z) mod Y  may_be_deduced_from [ Y < Z, Z <= 0 ].

modular(21):  (X * Y + Z) mod Y <= 0  may_be_deduced_from [ Y < Z, Z <= 0 ].

 

/** Properties ***/

modular(30):   (X * Y + Z) mod Y = Z  may_be_deduced_from [ 0 <= Z, Z < Y ].

modular(31):   (X * Y + Z) mod Y = Z  may_be_deduced_from [ Z <= 0, Y < Z ].

 

modular(32):   N mod N       may_be_replaced_by  0     if [ N <> 0 ].

modular(33):   N mod N       may_be_replaced_by  0     if [ N > 0 ].

modular(34):   N mod N       may_be_replaced_by  0     if [ N < 0 ].

 

modular(40):   X * Y mod Y   may_be_replaced_by  0     if [ Y <> 0 ].

modular(41):   X mod Y       may_be_replaced_by  X     if [ 0 <= X, X < Y ].

modular(42):   X mod Y       may_be_replaced_by  X     if [ Y < X,  X <= 0 ].

 

modular(50):   X mod Y mod Z = X mod Y may_be_deduced_from

                                          [ 0 <= B, B < Y, Y <= Z, X = A*Y + B ].

modular(51):   X mod Y mod Z = X mod Y may_be_deduced_from

                                          [ Z <= Y, Y < B, B <= 0, X = A*Y + B ].

 

modular(52):   X mod Y mod Z = X mod Z may_be_deduced_from

                             [ X = A * Y + B, B = C * Z + D, Y = Z * E,

                               0 <= B, B < Y,  0 <= D, D < Z ].

 

modular(53):   X mod Y mod Z = X mod Z may_be_deduced_from

                             [ X = A * Y + B, B = C * Z + D, Y = Z * E,

                               0 <= B, B < Y,  D <= 0, Z < D ].

 

modular(54):   X mod Y mod Z = X mod Z may_be_deduced_from

                             [ X = A * Y + B, B = C * Z + D, Y = Z * E,

                               B <= 0, Y < B,  0 <= D, D < Z ].

 

modular(55):   X mod Y mod Z = X mod Z may_be_deduced_from

                             [ X = A * Y + B, B = C * Z + D, Y = Z * E,

                               B <= 0, Y < B,  D <= 0, Z < 0 ].

 

modular(60):   X mod Y = -((-X) mod (-Y)) may_be_deduced_from

                                            [ 0 <= B, B < Y, X = A * Y + B ].

modular(61):   X mod Y = -((-X) mod (-Y)) may_be_deduced_from

                                            [ Y < B, B <= 0, X = A * Y + B ].


4.12          QUANTIF.RUL

%-------------------------------------------------------------------------------

%  (C) Altran Praxis Limited

%-------------------------------------------------------------------------------

%

%  The SPARK toolset is free software; you can redistribute it and/or modify it

%  under terms of the GNU General Public License as published by the Free

%  Software Foundation; either version 3, or (at your option) any later

%  version. The SPARK toolset is distributed in the hope that it will be

%  useful, but WITHOUT ANY WARRANTY; without even the implied warranty of

%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General

%  Public License for more details. You should have received a copy of the GNU

%  General Public License distributed with the SPARK toolset; see file

%  COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of

%  the license.

%

%===============================================================================

 

%-------------------------------------------------------------------------------

% RULE FAMILY CONTAINED HEREIN :-

%

% quant        : rules for quantified expressions

%-------------------------------------------------------------------------------

% MODEL DECLARATION FOR THIS FILE :-

%

% rule_family quant:

%         for_all(X, Y)  requires [ X:any, Y:any ] &

%         not X          requires [ X:any        ] &

%         for_some(X, Y) requires [ X:any, Y:any ] &

%         X or Y         requires [ X:any, Y:any ].

%-------------------------------------------------------------------------------

 

/*** COMMON QUANTIFICATION TECHNIQUES ***/

 

/*** Rewriting of quantified terms ***/

 

quant(1):   for_all(X,Y) & (not for_some(X,not Y)) are_interchangeable.

quant(2):   for_all(X,not Y) & (not for_some(X,Y)) are_interchangeable.

quant(3):   for_some(X,Y) & (not for_all(X,not Y)) are_interchangeable.

quant(4):   for_some(X,not Y) & (not for_all(X,Y)) are_interchangeable.

quant(5):   for_all(X,for_all(Y,P)) & for_all(Y,for_all(X,P))

                  are_interchangeable.

quant(6):   for_some(X,for_some(Y,P)) & for_some(Y,for_some(X,P))

                  are_interchangeable.

quant(7):   for_some(Y,for_all(X,P)) may_be_replaced_by

             for_all(X,for_some(Y,P)).

 

/*** Simple inferences ***/

 

quant(8):   for_some(X,P) may_be_deduced_from [ for_all(X,P) ].

 

 

/*** Inferences involving ‘AND’ ***/

 

quant(9):   for_all(X,A) may_be_deduced_from [ for_all(X,A and B) ].

quant(10):  for_all(X,B) may_be_deduced_from [ for_all(X,A and B) ].

quant(11):  for_all(X,A and B) may_be_deduced_from

                  [ for_all(X,A), for_all(X,B) ].

quant(12):  for_some(X,A) may_be_deduced_from [ for_some(X,A and B) ].

quant(13):  for_some(X,B) may_be_deduced_from [ for_some(X,A and B) ].

 

 

/*** Inferences involving ‘OR’ ***/

 

quant(14):  for_some(X,A or B) may_be_deduced_from [ for_some(X,A) ].

quant(15):  for_some(X,A or B) may_be_deduced_from [ for_some(X,B) ].

quant(16):  for_some(X,A) or for_some(X,B) may_be_deduced_from

                  [ for_some(X,A or B) ].

quant(17):  for_all(X,A or B) may_be_deduced_from [ for_all(X,A) ].

quant(18):  for_all(X,A or B) may_be_deduced_from [ for_all(X,B) ].

 

 

/*** Inferences involving ‘->’ ***/

 

quant(19):  for_some(X,A -> B) may_be_deduced_from [ for_some(X,not A) ].

quant(20):  for_some(X,A -> B) may_be_deduced_from [ for_some(X,B) ].

quant(21):  for_some(X,not A) or for_some(X,B) may_be_deduced_from

                  [ for_some(X,A -> B) ].

quant(22):  for_all(X,A -> B) may_be_deduced_from [ for_all(X,not A) ].

quant(23):  for_all(X,A -> B) may_be_deduced_from [ for_all(X,B) ].

 

 

/*** Inferences involving ‘<->’ ***/

 

quant(24):  for_all(X,A -> B) may_be_deduced_from [ for_all(X,A <-> B) ].

quant(25):  for_all(X,B -> A) may_be_deduced_from [ for_all(X,A <-> B) ].

quant(26):  for_all(X,A <-> B) may_be_deduced_from

                  [ for_all(X,A -> B), for_all(X,B -> A) ].

quant(27):  for_some(X,A -> B) may_be_deduced_from [ for_some(X,A <-> B) ].

quant(28):  for_some(X,B -> A) may_be_deduced_from [ for_some(X,A <-> B) ].


4.13          RECORD.RUL

%-------------------------------------------------------------------------------

%  (C) Altran Praxis Limited

%-------------------------------------------------------------------------------

%

%  The SPARK toolset is free software; you can redistribute it and/or modify it

%  under terms of the GNU General Public License as published by the Free

%  Software Foundation; either version 3, or (at your option) any later

%  version. The SPARK toolset is distributed in the hope that it will be

%  useful, but WITHOUT ANY WARRANTY; without even the implied warranty of

%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General

%  Public License for more details. You should have received a copy of the GNU

%  General Public License distributed with the SPARK toolset; see file

%  COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of

%  the license.

%

%===============================================================================

 

%-------------------------------------------------------------------------------

% RULE FAMILIES CONTAINED HEREIN :-

%

% record          : record-type simplification rules

% record_equality : equality of two record-type objects

% mk__record      : rules specific to SPARK record aggregates

%-------------------------------------------------------------------------------

% MODEL DECLARATIONS FOR THIS FILE :-

%

% rule_family record:

%         X requires [ X:any ].

%

% rule_family record_equality:

%         X=Y requires [ X:any, Y:any ].

%

% rule_family mk__record:

%         X requires [ X:any ].

%-------------------------------------------------------------------------------

 

/*** RECORD SIMPLIFICATION rules ***/

 

/* record(1): fld_F(upf_F(_, VALUE)) may_be_replaced_by VALUE. */

RECORD1:    FLD may_be_replaced_by VALUE if

                [ goal(nonvar(RECORD1)),

                  goal(RECORD1=record(1)),

                  goal(record_function(_, FLD, access, F, [RECORD], TYPE)),

                  goal(record_function(_, RECORD, update, F, [_, VALUE], TYPE)) ].

 

/* record(2): upf_F(REC, fld_F(REC)) may_be_replaced_by REC. */

RECORD2:    UPF may_be_replaced_by REC if

                [ goal(nonvar(RECORD2)),

                  goal(RECORD2=record(2)),

                  goal(record_function(_, UPF, update, F, [REC, VALUE], TYPE)),

                  goal(record_function(_, VALUE, access, F, [REC], TYPE)) ].

 

/* record(3): upf_F(upf_G(R,VG),VF) may_be_replaced_by upf_G(upf_F(R,VF),VG) if [ "F" <> "G" ]. */

RECORD3:    UPF_F may_be_replaced_by UPF_G if

                [ goal(nonvar(RECORD3)),

                  goal(RECORD3=record(3)),

                  goal(record_function(_, UPF_F, update, F, [REC1, VF], TYPE)),

                  goal(record_function(_, REC1,  update, G, [R, VG], TYPE)),

                  goal(F \= G),

                  goal(record_function(_, REC2,  update, F, [R, VF], TYPE)),

                  goal(record_function(_, UPF_G, update, G, [REC2, VG], TYPE)) ].

 

/* record(4): fld_F(upf_G(R, V)) may_be_replaced_by fld_F(R) if [ "F" <> "G" ]. */

RECORD4:    FLD_F_UPF_G may_be_replaced_by FLD_F_R if

                [ goal(nonvar(RECORD4)),

                  goal(RECORD4=record(4)),

                  goal(record_function(_, FLD_F_UPF_G, access, F, [UPF_G], TYPE)),

                  goal(record_function(_, UPF_G, update, G, [R, V], TYPE)),

                  goal(F \= G),

                  goal(record_function(_, FLD_F_R, access, F, [R], TYPE)) ].

 

/* record(5): upf_F(upf_F(R, _), V) may_be_replaced_by upf_F(R, V). */

RECORD5:    UPF_F_UPF_F_R may_be_replaced_by UPF_F_R if

                [ goal(nonvar(RECORD5)),

                  goal(RECORD5=record(5)),

                  goal(record_function(_, UPF_F_UPF_F_R, update, F, [UPF_F, V], TYPE)),

                  goal(record_function(_, UPF_F, update, F, [R, _], TYPE)),

                  goal(record_function(_, UPF_F_R, update, F, [R, V], TYPE)) ].

 

 

 

/*** RECORD EQUALITY RULES ***/

 

/* record_equality(1): {for records with ONE field}

        R=S may_be_deduced_from [ fld_F1(R)=fld_F1(S) ]. */

RECORD_EQUALITY1:

        R = S may_be_deduced_from

                [ goal(nonvar(RECORD_EQUALITY1)),

                  goal(RECORD_EQUALITY1=record_equality(1)),

                  goal(checktype(R,RECORD_TYPE)),

                  goal(type(RECORD_TYPE, record([[F1,_]]))),

                  goal(checktype(S,RECORD_TYPE)),

                  goal(record_function(_, R1, access, F1, [R], RECORD_TYPE)),

                  goal(record_function(_, S1, access, F1, [S], RECORD_TYPE)),

                  R1 = S1 ].

 

/* record_equality(2): {for records with TWO fields}

        R=S may_be_deduced_from [ fld_F1(R)=fld_F1(S), fld_F2(R)=fld_F2(S) ]. */

RECORD_EQUALITY2:

        R = S may_be_deduced_from

                [ goal(nonvar(RECORD_EQUALITY2)),

                  goal(RECORD_EQUALITY2=record_equality(2)),

                  goal(checktype(R,RECORD_TYPE)),

                  goal(type(RECORD_TYPE, record([[F1,_],[F2,_]]))),

                  goal(checktype(S,RECORD_TYPE)),

                  goal(record_function(_, R1, access, F1, [R], RECORD_TYPE)),

                  goal(record_function(_, S1, access, F1, [S], RECORD_TYPE)),

                  goal(record_function(_, R2, access, F2, [R], RECORD_TYPE)),

                  goal(record_function(_, S2, access, F2, [S], RECORD_TYPE)),

                  R1 = S1, R2 = S2 ].

 

/* record_equality(3): {for records with THREE fields}

        R=S may_be_deduced_from

           [ fld_F1(R)=fld_F1(S), fld_F2(R)=fld_F2(S), fld_F3(R)=fld_F3(S) ]. */

RECORD_EQUALITY3:

        R = S may_be_deduced_from

                [ goal(nonvar(RECORD_EQUALITY3)),

                  goal(RECORD_EQUALITY3=record_equality(3)),

                  goal(checktype(R,RECORD_TYPE)),

                  goal(type(RECORD_TYPE, record([[F1,_],[F2,_],[F3,_]]))),

                  goal(checktype(S,RECORD_TYPE)),

                  goal(record_function(_, R1, access, F1, [R], RECORD_TYPE)),

                  goal(record_function(_, S1, access, F1, [S], RECORD_TYPE)),

                  goal(record_function(_, R2, access, F2, [R], RECORD_TYPE)),

                  goal(record_function(_, S2, access, F2, [S], RECORD_TYPE)),

                  goal(record_function(_, R3, access, F3, [R], RECORD_TYPE)),

                  goal(record_function(_, S3, access, F3, [S], RECORD_TYPE)),

                  R1 = S1, R2 = S2, R3 = S3 ].

 

/* record_equality(4): {for records with FOUR fields}

        R=S may_be_deduced_from

           [ fld_F1(R)=fld_F1(S), fld_F2(R)=fld_F2(S),

             fld_F3(R)=fld_F3(S), fld_F4(R)=fld_F4(S) ]. */

RECORD_EQUALITY4:

        R = S may_be_deduced_from

                [ goal(nonvar(RECORD_EQUALITY4)),

                  goal(RECORD_EQUALITY4=record_equality(4)),

                  goal(checktype(R,RECORD_TYPE)),

                  goal(type(RECORD_TYPE,

                        record([[F1,_],[F2,_],[F3,_],[F4,_]]))),

                  goal(checktype(S,RECORD_TYPE)),

                  goal(record_function(_, R1, access, F1, [R], RECORD_TYPE)),

                  goal(record_function(_, S1, access, F1, [S], RECORD_TYPE)),

                  goal(record_function(_, R2, access, F2, [R], RECORD_TYPE)),

                  goal(record_function(_, S2, access, F2, [S], RECORD_TYPE)),

                  goal(record_function(_, R3, access, F3, [R], RECORD_TYPE)),

                  goal(record_function(_, S3, access, F3, [S], RECORD_TYPE)),

                  goal(record_function(_, R4, access, F4, [R], RECORD_TYPE)),

                  goal(record_function(_, S4, access, F4, [S], RECORD_TYPE)),

                  R1 = S1, R2 = S2, R3 = S3, R4 = S4 ].

 

/* record_equality(5): {for records with FIVE fields}

        R=S may_be_deduced_from

           [ fld_F1(R)=fld_F1(S), fld_F2(R)=fld_F2(S),

             fld_F3(R)=fld_F3(S), fld_F4(R)=fld_F4(S),

             fld_F5(R)=fld_F5(S) ]. */

RECORD_EQUALITY5:

        R = S may_be_deduced_from

                [ goal(nonvar(RECORD_EQUALITY5)),

                  goal(RECORD_EQUALITY5=record_equality(5)),

                  goal(checktype(R,RECORD_TYPE)),

                  goal(type(RECORD_TYPE,

                        record([[F1,_],[F2,_],[F3,_],[F4,_],[F5,_]]))),

                  goal(checktype(S,RECORD_TYPE)),

                  goal(record_function(_, R1, access, F1, [R], RECORD_TYPE)),

                  goal(record_function(_, S1, access, F1, [S], RECORD_TYPE)),

                  goal(record_function(_, R2, access, F2, [R], RECORD_TYPE)),

                  goal(record_function(_, S2, access, F2, [S], RECORD_TYPE)),

                  goal(record_function(_, R3, access, F3, [R], RECORD_TYPE)),

                  goal(record_function(_, S3, access, F3, [S], RECORD_TYPE)),

                  goal(record_function(_, R4, access, F4, [R], RECORD_TYPE)),

                  goal(record_function(_, S4, access, F4, [S], RECORD_TYPE)),

                  goal(record_function(_, R5, access, F5, [R], RECORD_TYPE)),

                  goal(record_function(_, S5, access, F5, [S], RECORD_TYPE)),

                  R1 = S1, R2 = S2, R3 = S3, R4 = S4, R5 = S5 ].

 

/* record_equality(6): {for records with SIX fields}

        R=S may_be_deduced_from

           [ fld_F1(R)=fld_F1(S), fld_F2(R)=fld_F2(S),

             fld_F3(R)=fld_F3(S), fld_F4(R)=fld_F4(S),

             fld_F5(R)=fld_F5(S), fld_F6(R)=fld_F6(S) ]. */

RECORD_EQUALITY6:

        R = S may_be_deduced_from

                [ goal(nonvar(RECORD_EQUALITY6)),

                  goal(RECORD_EQUALITY6=record_equality(6)),

                  goal(checktype(R,RECORD_TYPE)),

                  goal(type(RECORD_TYPE,

                        record([[F1,_],[F2,_],[F3,_],[F4,_],[F5,_],[F6,_]]))),

                  goal(checktype(S,RECORD_TYPE)),

                  goal(record_function(_, R1, access, F1, [R], RECORD_TYPE)),

                  goal(record_function(_, S1, access, F1, [S], RECORD_TYPE)),

                  goal(record_function(_, R2, access, F2, [R], RECORD_TYPE)),

                  goal(record_function(_, S2, access, F2, [S], RECORD_TYPE)),

                  goal(record_function(_, R3, access, F3, [R], RECORD_TYPE)),

                  goal(record_function(_, S3, access, F3, [S], RECORD_TYPE)),

                  goal(record_function(_, R4, access, F4, [R], RECORD_TYPE)),

                  goal(record_function(_, S4, access, F4, [S], RECORD_TYPE)),

                  goal(record_function(_, R5, access, F5, [R], RECORD_TYPE)),

                  goal(record_function(_, S5, access, F5, [S], RECORD_TYPE)),

                  goal(record_function(_, R6, access, F6, [R], RECORD_TYPE)),

                  goal(record_function(_, S6, access, F6, [S], RECORD_TYPE)),

                  R1 = S1, R2 = S2, R3 = S3, R4 = S4, R5 = S5, R6 = S6 ].

 

/* record_equality(7): {for records with SEVEN fields}

        R=S may_be_deduced_from

           [ fld_F1(R)=fld_F1(S), fld_F2(R)=fld_F2(S),

             fld_F3(R)=fld_F3(S), fld_F4(R)=fld_F4(S),

             fld_F5(R)=fld_F5(S), fld_F6(R)=fld_F6(S),

             fld_F7(R)=fld_F7(S) ]. */

RECORD_EQUALITY7:

        R = S may_be_deduced_from

                [ goal(nonvar(RECORD_EQUALITY7)),

                  goal(RECORD_EQUALITY7=record_equality(7)),

                  goal(checktype(R,RECORD_TYPE)),

                  goal(type(RECORD_TYPE,

                        record([[F1,_],[F2,_],[F3,_],[F4,_],[F5,_],[F6,_],

                                [F7,_]]))),

                  goal(checktype(S,RECORD_TYPE)),

                  goal(record_function(_, R1, access, F1, [R], RECORD_TYPE)),

                  goal(record_function(_, S1, access, F1, [S], RECORD_TYPE)),

                  goal(record_function(_, R2, access, F2, [R], RECORD_TYPE)),

                  goal(record_function(_, S2, access, F2, [S], RECORD_TYPE)),

                  goal(record_function(_, R3, access, F3, [R], RECORD_TYPE)),

                  goal(record_function(_, S3, access, F3, [S], RECORD_TYPE)),

                  goal(record_function(_, R4, access, F4, [R], RECORD_TYPE)),

                  goal(record_function(_, S4, access, F4, [S], RECORD_TYPE)),

                  goal(record_function(_, R5, access, F5, [R], RECORD_TYPE)),

                  goal(record_function(_, S5, access, F5, [S], RECORD_TYPE)),

                  goal(record_function(_, R6, access, F6, [R], RECORD_TYPE)),

                  goal(record_function(_, S6, access, F6, [S], RECORD_TYPE)),

                  goal(record_function(_, R7, access, F7, [R], RECORD_TYPE)),

                  goal(record_function(_, S7, access, F7, [S], RECORD_TYPE)),

                  R1=S1, R2=S2, R3=S3, R4=S4, R5=S5, R6=S6, R7=S7 ].

 

/* record_equality(8): {for records with EIGHT fields}

        R=S may_be_deduced_from

           [ fld_F1(R)=fld_F1(S), fld_F2(R)=fld_F2(S),

             fld_F3(R)=fld_F3(S), fld_F4(R)=fld_F4(S),

             fld_F5(R)=fld_F5(S), fld_F6(R)=fld_F6(S),

             fld_F7(R)=fld_F7(S), fld_F8(R)=fld_F8(S) ]. */

RECORD_EQUALITY8:

        R = S may_be_deduced_from

                [ goal(nonvar(RECORD_EQUALITY8)),

                  goal(RECORD_EQUALITY8=record_equality(8)),

                  goal(checktype(R,RECORD_TYPE)),

                  goal(type(RECORD_TYPE,

                        record([[F1,_],[F2,_],[F3,_],[F4,_],[F5,_],[F6,_],

                                [F7,_],[F8,_]]))),

                  goal(checktype(S,RECORD_TYPE)),

                  goal(record_function(_, R1, access, F1, [R], RECORD_TYPE)),

                  goal(record_function(_, S1, access, F1, [S], RECORD_TYPE)),

                  goal(record_function(_, R2, access, F2, [R], RECORD_TYPE)),

                  goal(record_function(_, S2, access, F2, [S], RECORD_TYPE)),

                  goal(record_function(_, R3, access, F3, [R], RECORD_TYPE)),

                  goal(record_function(_, S3, access, F3, [S], RECORD_TYPE)),

                  goal(record_function(_, R4, access, F4, [R], RECORD_TYPE)),

                  goal(record_function(_, S4, access, F4, [S], RECORD_TYPE)),

                  goal(record_function(_, R5, access, F5, [R], RECORD_TYPE)),

                  goal(record_function(_, S5, access, F5, [S], RECORD_TYPE)),

                  goal(record_function(_, R6, access, F6, [R], RECORD_TYPE)),

                  goal(record_function(_, S6, access, F6, [S], RECORD_TYPE)),

                  goal(record_function(_, R7, access, F7, [R], RECORD_TYPE)),

                  goal(record_function(_, S7, access, F7, [S], RECORD_TYPE)),

                  goal(record_function(_, R8, access, F8, [R], RECORD_TYPE)),

                  goal(record_function(_, S8, access, F8, [S], RECORD_TYPE)),

                  R1=S1, R2=S2, R3=S3, R4=S4, R5=S5, R6=S6, R7=S7, R8=S8 ].

 

/* record_equality(9): {for records with NINE fields}

        R=S may_be_deduced_from

           [ fld_F1(R)=fld_F1(S), fld_F2(R)=fld_F2(S),

             fld_F3(R)=fld_F3(S), fld_F4(R)=fld_F4(S),

             fld_F5(R)=fld_F5(S), fld_F6(R)=fld_F6(S),

             fld_F7(R)=fld_F7(S), fld_F8(R)=fld_F8(S),

             fld_F9(R)=fld_F9(S) ]. */

RECORD_EQUALITY9:

        R = S may_be_deduced_from

                [ goal(nonvar(RECORD_EQUALITY9)),

                  goal(RECORD_EQUALITY9=record_equality(9)),

                  goal(checktype(R,RECORD_TYPE)),

                  goal(type(RECORD_TYPE,

                        record([[F1,_],[F2,_],[F3,_],[F4,_],[F5,_],[F6,_],

                                [F7,_],[F8,_],[F9,_]]))),

                  goal(checktype(S,RECORD_TYPE)),

                  goal(record_function(_, R1, access, F1, [R], RECORD_TYPE)),

                  goal(record_function(_, S1, access, F1, [S], RECORD_TYPE)),

                  goal(record_function(_, R2, access, F2, [R], RECORD_TYPE)),

                  goal(record_function(_, S2, access, F2, [S], RECORD_TYPE)),

                  goal(record_function(_, R3, access, F3, [R], RECORD_TYPE)),

                  goal(record_function(_, S3, access, F3, [S], RECORD_TYPE)),

                  goal(record_function(_, R4, access, F4, [R], RECORD_TYPE)),

                  goal(record_function(_, S4, access, F4, [S], RECORD_TYPE)),

                  goal(record_function(_, R5, access, F5, [R], RECORD_TYPE)),

                  goal(record_function(_, S5, access, F5, [S], RECORD_TYPE)),

                  goal(record_function(_, R6, access, F6, [R], RECORD_TYPE)),

                  goal(record_function(_, S6, access, F6, [S], RECORD_TYPE)),

                  goal(record_function(_, R7, access, F7, [R], RECORD_TYPE)),

                  goal(record_function(_, S7, access, F7, [S], RECORD_TYPE)),

                  goal(record_function(_, R8, access, F8, [R], RECORD_TYPE)),

                  goal(record_function(_, S8, access, F8, [S], RECORD_TYPE)),

                  goal(record_function(_, R9, access, F9, [R], RECORD_TYPE)),

                  goal(record_function(_, S9, access, F9, [S], RECORD_TYPE)),

                  R1=S1, R2=S2, R3=S3, R4=S4, R5=S5, R6=S6, R7=S7, R8=S8,

                  R9=S9 ].

 

/* record_equality(10): {for records with TEN fields}

        R=S may_be_deduced_from

           [ fld_F1(R)=fld_F1(S), fld_F2(R)=fld_F2(S),

             fld_F3(R)=fld_F3(S), fld_F4(R)=fld_F4(S),

             fld_F5(R)=fld_F5(S), fld_F6(R)=fld_F6(S),

             fld_F7(R)=fld_F7(S), fld_F8(R)=fld_F8(S),

             fld_F9(R)=fld_F9(S), fld_F10(R)=fld_F10(S) ]. */

RECORD_EQUALITY10:

        R = S may_be_deduced_from

                [ goal(nonvar(RECORD_EQUALITY10)),

                  goal(RECORD_EQUALITY10=record_equality(10)),

                  goal(checktype(R,RECORD_TYPE)),

                  goal(type(RECORD_TYPE,

                        record([[F1,_],[F2,_],[F3,_],[F4,_],[F5,_],[F6,_],

                                [F7,_],[F8,_],[F9,_],[F10,_]]))),

                  goal(checktype(S,RECORD_TYPE)),

                  goal(record_function(_, R1, access, F1, [R], RECORD_TYPE)),

                  goal(record_function(_, S1, access, F1, [S], RECORD_TYPE)),

                  goal(record_function(_, R2, access, F2, [R], RECORD_TYPE)),

                  goal(record_function(_, S2, access, F2, [S], RECORD_TYPE)),

                  goal(record_function(_, R3, access, F3, [R], RECORD_TYPE)),

                  goal(record_function(_, S3, access, F3, [S], RECORD_TYPE)),

                  goal(record_function(_, R4, access, F4, [R], RECORD_TYPE)),

                  goal(record_function(_, S4, access, F4, [S], RECORD_TYPE)),

                  goal(record_function(_, R5, access, F5, [R], RECORD_TYPE)),

                  goal(record_function(_, S5, access, F5, [S], RECORD_TYPE)),

                  goal(record_function(_, R6, access, F6, [R], RECORD_TYPE)),

                  goal(record_function(_, S6, access, F6, [S], RECORD_TYPE)),

                  goal(record_function(_, R7, access, F7, [R], RECORD_TYPE)),

                  goal(record_function(_, S7, access, F7, [S], RECORD_TYPE)),

                  goal(record_function(_, R8, access, F8, [R], RECORD_TYPE)),

                  goal(record_function(_, S8, access, F8, [S], RECORD_TYPE)),

                  goal(record_function(_, R9, access, F9, [R], RECORD_TYPE)),

                  goal(record_function(_, S9, access, F9, [S], RECORD_TYPE)),

                  goal(record_function(_, R10, access, F10, [R], RECORD_TYPE)),

                  goal(record_function(_, S10, access, F10, [S], RECORD_TYPE)),

                  R1=S1, R2=S2, R3=S3, R4=S4, R5=S5, R6=S6, R7=S7, R8=S8,

                  R9=S9, R10=S10 ].

 

/* record_equality(11): {for records with ELEVEN or more fields}

        R=S may_be_deduced_from

           [ fld_F1(R)=fld_F1(S), fld_F2(R)=fld_F2(S),

             fld_F3(R)=fld_F3(S), fld_F4(R)=fld_F4(S),

             fld_F5(R)=fld_F5(S), fld_F6(R)=fld_F6(S),

             fld_F7(R)=fld_F7(S), fld_F8(R)=fld_F8(S),

             fld_F9(R)=fld_F9(S), fld_F10(R)=fld_F10(S), ... ]. */

RECORD_EQUALITY11:

        R = S may_be_deduced_from

                [ goal(nonvar(RECORD_EQUALITY11)),

                  goal(RECORD_EQUALITY11=record_equality(11)),

                  goal(checktype(R,RECORD_TYPE)),

                  goal(type(RECORD_TYPE,record(FIELD_LIST))),

                  goal(length(FIELD_LIST, NO_OF_FIELDS)),

                  goal(NO_OF_FIELDS > 10),

                  goal(checktype(S,RECORD_TYPE)),

                  goal(make_record_equality_goal(FIELD_LIST,R,S,GOAL)),

                  GOAL ].

 

 

/* mk__record(1):

       fld_FIELD(mk__record(LARGS...(FIELD := VALUE)...))

              may_be_replaced_by VALUE if

              [ \+ ((FIELD := ...) is_in LARGS),

                \+ ((FIELD := ...) is_in RARGS) ].

       N.B.: Side conditions check uniqueness of assignment to FIELD. */

MK__RECORD1:

       FLD_FIELD_MK__RECORD_LARGS_FIELD_VALUE_RARGS may_be_replaced_by VALUE if

              [ goal(nonvar(MK__RECORD1)),

                goal(MK__RECORD1 = mk__record(1)),

                goal(record_function(_,

                     FLD_FIELD_MK__RECORD_LARGS_FIELD_VALUE_RARGS,

                     access, FIELD, [MK__RECORD_LARGS_FIELD_VALUE_RARGS], _)),

                goal(nonvar(MK__RECORD_LARGS_FIELD_VALUE_RARGS)),

                goal(MK__RECORD_LARGS_FIELD_VALUE_RARGS =..

                     [mk__record|LARGS_FIELD_VALUE_RARGS]),

                goal(append(LARGS, [(FIELD := VALUE)|RARGS],

                     LARGS_FIELD_VALUE_RARGS)),

                goal(\+ is_in((FIELD := _), LARGS)),

                goal(\+ is_in((FIELD := _), RARGS)) ].

 

 

/* mk__record(2):

       upf_FIELD(mk__record(LARGS...(FIELD := OLDVAL)...RARGS), NEWVAL)

              may_be_replaced_by

       mk__record(LARGS...(FIELD := NEWVAL)...RARGS) if

              [ \+ ((FIELD := ...) is_in LARGS),

                \+ ((FIELD := ...) is_in RARGS) ].

       N.B.: Side conditions check uniqueness of assignment to FIELD. */

MK__RECORD2:

       UPF_FIELD_MK__RECORD_LARGS_FIELD_OLDVAL_RARGS_NEWVAL

              may_be_replaced_by

       MK__RECORD_LARGS_FIELD_NEWVAL_RARGS if

              [ goal(nonvar(MK__RECORD2)),

                goal(MK__RECORD2 = mk__record(2)),

                goal(record_function(_,

                     UPF_FIELD_MK__RECORD_LARGS_FIELD_OLDVAL_RARGS_NEWVAL,

                     update, FIELD,

                     [MK__RECORD_LARGS_FIELD_OLDVAL_RARGS, NEWVAL], _)),

                goal(nonvar(MK__RECORD_LARGS_FIELD_OLDVAL_RARGS)),

                goal(MK__RECORD_LARGS_FIELD_OLDVAL_RARGS =..

                     [mk__record|LARGS_FIELD_OLDVAL_RARGS]),

                goal(append(LARGS, [(FIELD := OLDVAL)|RARGS],

                     LARGS_FIELD_OLDVAL_RARGS)),

                goal(\+ is_in((FIELD := _), LARGS)),

                goal(\+ is_in((FIELD := _), RARGS)),

                goal(append(LARGS, [(FIELD := NEWVAL)|RARGS],

                     LARGS_FIELD_NEWVAL_RARGS)),

                goal(MK__RECORD_LARGS_FIELD_NEWVAL_RARGS =..

                     [mk__record|LARGS_FIELD_NEWVAL_RARGS]) ].

 

 

/* mk__record(3):

       fld_FIELD(mk__RECORDTYPE(LARGS...(FIELD := VALUE)...))

              may_be_replaced_by VALUE if

              [ \+ ((FIELD := ...) is_in LARGS),

                \+ ((FIELD := ...) is_in RARGS) ].

       N.B.: Side conditions check uniqueness of assignment to FIELD. */

MK__RECORD3:

       FLD_FIELD_MK__RECORD_LARGS_FIELD_VALUE_RARGS may_be_replaced_by VALUE if

              [ goal(nonvar(MK__RECORD3)),

                goal(MK__RECORD3 = mk__record(3)),

                goal(record_function(_,

                     FLD_FIELD_MK__RECORD_LARGS_FIELD_VALUE_RARGS,

                     access, FIELD, [MK__RECORD_LARGS_FIELD_VALUE_RARGS], _)),

                goal(nonvar(MK__RECORD_LARGS_FIELD_VALUE_RARGS)),

                goal(MK__RECORD_LARGS_FIELD_VALUE_RARGS =..

                     [MK__RECORDTYPE|LARGS_FIELD_VALUE_RARGS]),

                goal(mk__function_name(MK__RECORDTYPE, _, record)),

                goal(append(LARGS, [(FIELD := VALUE)|RARGS],

                     LARGS_FIELD_VALUE_RARGS)),

                goal(\+ is_in((FIELD := _), LARGS)),

                goal(\+ is_in((FIELD := _), RARGS)) ].

 

 

/* mk__record(4):

       upf_FIELD(mk__RECORDTYPE(LARGS...(FIELD := OLDVAL)...RARGS), NEWVAL)

              may_be_replaced_by

       mk__RECORDTYPE(LARGS...(FIELD := NEWVAL)...RARGS) if

              [ \+ ((FIELD := ...) is_in LARGS),

                \+ ((FIELD := ...) is_in RARGS) ].

       N.B.: Side conditions check uniqueness of assignment to FIELD. */

MK__RECORD4:

       UPF_FIELD_MK__RECORD_LARGS_FIELD_OLDVAL_RARGS_NEWVAL

              may_be_replaced_by

       MK__RECORD_LARGS_FIELD_NEWVAL_RARGS if

              [ goal(nonvar(MK__RECORD4)),

                goal(MK__RECORD4 = mk__record(4)),

                goal(record_function(_,

                     UPF_FIELD_MK__RECORD_LARGS_FIELD_OLDVAL_RARGS_NEWVAL,

                     update, FIELD,

                     [MK__RECORD_LARGS_FIELD_OLDVAL_RARGS, NEWVAL], _)),

                goal(nonvar(MK__RECORD_LARGS_FIELD_OLDVAL_RARGS)),

                goal(MK__RECORD_LARGS_FIELD_OLDVAL_RARGS =..

                     [MK__RECORDTYPE|LARGS_FIELD_OLDVAL_RARGS]),

                goal(mk__function_name(MK__RECORDTYPE, _, record)),

                goal(append(LARGS, [(FIELD := OLDVAL)|RARGS],

                     LARGS_FIELD_OLDVAL_RARGS)),

                goal(\+ is_in((FIELD := _), LARGS)),

                goal(\+ is_in((FIELD := _), RARGS)),

                goal(append(LARGS, [(FIELD := NEWVAL)|RARGS],

                     LARGS_FIELD_NEWVAL_RARGS)),

                goal(MK__RECORD_LARGS_FIELD_NEWVAL_RARGS =..

                     [MK__RECORDTYPE|LARGS_FIELD_NEWVAL_RARGS]) ].

 


4.14          SEQ.RUL

%-------------------------------------------------------------------------------

%  (C) Altran Praxis Limited

%-------------------------------------------------------------------------------

%

%  The SPARK toolset is free software; you can redistribute it and/or modify it

%  under terms of the GNU General Public License as published by the Free

%  Software Foundation; either version 3, or (at your option) any later

%  version. The SPARK toolset is distributed in the hope that it will be

%  useful, but WITHOUT ANY WARRANTY; without even the implied warranty of

%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General

%  Public License for more details. You should have received a copy of the GNU

%  General Public License distributed with the SPARK toolset; see file

%  COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of

%  the license.

%

%===============================================================================

%-------------------------------------------------------------------------------

% RULE FAMILIES CONTAINED HEREIN :-

%

% seqlen       : properties of the length of sequence function

% append       : properties of the append operator

% first        : properties of the sequence function first

% last         : properties of the sequence function last

% nonfirst     : properties of the sequence function nonfirst

% nonlast      : properties of the sequence function nonlast

% seq          : equality properties of sequences

%-------------------------------------------------------------------------------

% MODEL DECLARATIONS FOR THIS FILE :-

%

% rule_family seqlen:

%         X >= Y    requires [ X:i,   Y:i ] &

%         X > Y     requires [ X:i,   Y:i ] &

%         length(X) requires [ X:any      ] &

%         X + Y     requires [ X:i,   Y:i ] &

%         X - Y     requires [ X:i,   Y:i ].

%

% rule_family append:

%         X @ Y     requires [ X:any, Y:any ].

%

% rule_family first:

%         first(X)    requires [ X:any ].

%

% rule_family last:

%         last(X)     requires [ X:any ].

%

% rule_family nonfirst:

%         nonfirst(X) requires [ X:any ] &

%         X @ Y       requires [ X:any, Y:any ].

%

% rule_family nonlast:

%         nonlast(X)  requires [ X:any ] &

%         [X|Y]       requires [ X:any, Y:any ] &

%         X @ Y       requires [ X:any, Y:any ].

%

% rule_family seq:

%         X <-> Y     requires [ X:any, Y:any ] &

%         X = Y       requires [ X:any, Y:any ].

%-------------------------------------------------------------------------------

/*** Sequence length rules ***/

seqlen(1):      length(S)>=0 may_be_deduced.

seqlen(2):      length([H|T])>0 may_be_deduced.

seqlen(3):      length([H|T])>=1 may_be_deduced.

seqlen(4):      length([]) may_be_replaced_by 0.

seqlen(5):      length([H|T]) may_be_replaced_by N if

                        [ goal(length([H|T],N)) ].

seqlen(6):      length(S @ T) & length(S)+length(T) are_interchangeable.

seqlen(7):      length(S) & length(nonlast(S))+1 are_interchangeable if

                        [ S<>[] ].

seqlen(8):      length(S) & length(nonlast(S))+1 are_interchangeable if

                        [ length(S)>=1 ].

seqlen(9):      length(S)-1 & length(nonlast(S)) are_interchangeable if

                        [ S<>[] ].

seqlen(10):      length(S)-1 & length(nonlast(S)) are_interchangeable if

                        [ length(S)>=1 ].

seqlen(11):      length(S) & length(nonfirst(S))+1 are_interchangeable if

                        [ S<>[] ].

seqlen(12):      length(S) & length(nonfirst(S))+1 are_interchangeable if

                        [ length(S)>=1 ].

seqlen(13):      length(S)-1 & length(nonfirst(S)) are_interchangeable if

                        [ S<>[] ].

seqlen(14):      length(S)-1 & length(nonfirst(S)) are_interchangeable if

                        [ length(S)>=1 ].

 

 

/*** Append rules ***/

append(1):      ([] @ L) may_be_replaced_by L.

append(2):      (L @ []) may_be_replaced_by L.

append(3):      ([H1|T1] @ [H2|T2]) may_be_replaced_by L if

                        [ goal(append([H1|T1],[H2|T2],L)) ].

append(4):      ([first(S)] @ nonfirst(S)) may_be_replaced_by S if [ S<>[] ].

append(5):      (nonlast(S) @ [last(S)])   may_be_replaced_by S if [ S<>[] ].

append(6):      ((X @ Y) @ Z) & (X @ (Y @ Z)) are_interchangeable.

 

 

/*** First rules ***/

first(1):       first([H|T]) may_be_replaced_by H.

first(2):       first([H|T] @ Y) may_be_replaced_by H.

first(3):       first(X @ Y) & first(X) are_interchangeable if [ X<>[] ].

 

/*** Last rules ***/

last(1):        last([H]) may_be_replaced_by H.

last(2):        last(X @ [H|T]) may_be_replaced_by last([H|T]).

last(3):        last([H|T]) & last(T) are_interchangeable if [ T<>[] ].

last(4):        last(X @ Y) & last(Y) are_interchangeable if [ Y<>[] ].

 

 

/*** Nonfirst rules ***/

nonfirst(1):    nonfirst([H|T]) may_be_replaced_by T.

nonfirst(2):    nonfirst(T) may_be_replaced_by [] if [ length(T)=1 ].

nonfirst(3):    nonfirst(X @ Y) & nonfirst(X) @ Y are_interchangeable if

                        [ X<>[] ].

nonfirst(4):    nonfirst([H|T] @ Y) may_be_replaced_by T @ Y.

 

 

/*** Nonlast rules ***/

nonlast(1):     nonlast([H]) may_be_replaced_by [].

nonlast(2):     nonlast(T) may_be_replaced_by [] if [ length(T)=1 ].

nonlast(3):     nonlast([H|T]) & [H|T1] are_interchangeable if

                        [ nonlast(T)=T1 ].

nonlast(4):     nonlast(X @ Y) & X @ nonlast(Y) are_interchangeable if

                        [ Y<>[] ].

nonlast(5):     nonlast(X @ [H]) may_be_replaced_by X.

 

/*** Sequence Equality rules ***/

seq(1):         X = Y <-> ((first(X)=first(Y) and nonfirst(X)=nonfirst(Y))

                       or (X=[] and Y=[]))

                        may_be_deduced.

seq(2):         X = Y may_be_deduced_from

                        [ first(X)=first(Y), nonfirst(X)=nonfirst(Y) ].

seq(3):         X = Y <-> ((nonlast(X)=nonlast(Y) and last(X)=last(Y))

                           or (X=[] and Y=[]))

                        may_be_deduced.

seq(4):         X = Y may_be_deduced_from

                        [ nonlast(X)=nonlast(Y), last(X)=last(Y) ].

 


4.15          SETS.RUL

%-------------------------------------------------------------------------------

%  (C) Altran Praxis Limited

%-------------------------------------------------------------------------------

%

%  The SPARK toolset is free software; you can redistribute it and/or modify it

%  under terms of the GNU General Public License as published by the Free

%  Software Foundation; either version 3, or (at your option) any later

%  version. The SPARK toolset is distributed in the hope that it will be

%  useful, but WITHOUT ANY WARRANTY; without even the implied warranty of

%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General

%  Public License for more details. You should have received a copy of the GNU

%  General Public License distributed with the SPARK toolset; see file

%  COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of

%  the license.

%

%===============================================================================

 

%-------------------------------------------------------------------------------

% RULE FAMILY CONTAINED HEREIN :-

%

% sets         : properties of FDL set types

%-------------------------------------------------------------------------------

% MODEL DECLARATION FOR THIS FILE :-

%

% rule_family sets:

%         X in Y               requires [ X:any, Y:any ] &

%         X not_in Y           requires [ X:any, Y:any ] &

%         not X                requires [ X:any        ] &

%         X \/ Y               requires [ X:any, Y:any ] &

%         X /\ Y               requires [ X:any, Y:any ] &

%         X \ Y                requires [ X:any, Y:any ] &

%         X or Y               requires [ X:any, Y:any ] &

%         X subset_of Y        requires [ X:any, Y:any ] &

%         X strict_subset_of Y requires [ X:any, Y:any ].

%-------------------------------------------------------------------------------

/*** Set rules ***/

 

/*** Element of ***/

sets(1):        X in (set A) may_be_deduced_from [ goal(is_in(X,A)) ].

sets(2):        (X not_in A) & (not (X in A)) are_interchangeable.

sets(3):        (X in A) & (not (X not_in A)) are_interchangeable.

 

/*** Union ***/

sets(4):        X in (A \/ B) may_be_deduced_from [ X in A ].

sets(5):        X in (A \/ B) may_be_deduced_from [ X in B ].

sets(6):        X not_in (A \/ B) may_be_deduced_from

                        [ X not_in A, X not_in B ].

sets(7):        A \/ B may_be_replaced_by A if [ B subset_of A ].

sets(8):        B \/ A may_be_replaced_by A if [ B subset_of A ].

sets(9):        A \/ (set []) may_be_replaced_by A if [].

sets(10):       (set []) \/ A may_be_replaced_by A if [].

sets(11):       (set A) \/ (set B) may_be_replaced_by (set C) if

                        [ goal(set_union(A,B,C)) ].

 

/*** Intersection ***/

sets(12):       X in (A /\ B) may_be_deduced_from [ X in A, X in B ].

sets(13):       X not_in (A /\ B) may_be_deduced_from [ X not_in A ].

sets(14):       X not_in (A /\ B) may_be_deduced_from [ X not_in B ].

sets(15):       A /\ B may_be_replaced_by A if [ A subset_of B ].

sets(16):       B /\ A may_be_replaced_by A if [ A subset_of B ].

sets(17):       (set []) /\ B may_be_replaced_by (set []) if [].

sets(18):       A /\ (set []) may_be_replaced_by (set []) if [].

sets(19):       ((set A) /\ (set B)) may_be_replaced_by (set C) if

                        [ goal(set_intersect(A,B,C)) ].

 

/*** ‘Lacking’ ***/

sets(20):       X in (A \ B) may_be_deduced_from [ X in A, X not_in B ].

sets(21):       X not_in (A \ B) may_be_deduced_from [ X not_in A ].

sets(22):       X not_in (A \ B) may_be_deduced_from [ X in B ].

sets(23):       (A \ B) may_be_replaced_by A if [ B=(set []) ].

sets(24):       (A \ B) may_be_replaced_by A if [ (A /\ B)=(set []) ].

sets(25):       (A \ B) may_be_replaced_by A if [ (B /\ A)=(set []) ].

sets(26):       (set A) \ (set B) may_be_replaced_by (set C) if

                        [ goal(set_lacking(A,B,C)) ].

sets(27):       X=E or X in S may_be_deduced_from

                        [ X in (set U), goal(is_in(E,U),

                          set_lacking(U,[E],S)) ].

 

/*** Empty set ***/

sets(28):       X not_in (set []) may_be_deduced.

 

/*** Subset rules ***/

sets(29):       (set []) subset_of A may_be_deduced.

sets(30):       A subset_of (A \/ B) may_be_deduced.

sets(31):       A subset_of (B \/ A) may_be_deduced.

sets(32):       (A /\ B) subset_of A may_be_deduced.

sets(33):       (B /\ A) subset_of A may_be_deduced.

sets(34):       (A \ B) subset_of A may_be_deduced.

sets(35):       A subset_of B may_be_deduced_from [ A strict_subset_of B ].

sets(36):       (set A) subset_of (set B) may_be_deduced_from

                        [ goal(subset(A,B)) ].

 

/*** Strict subset rule ***/

sets(37):       A strict_subset_of B may_be_deduced_from

                        [ A subset_of B, A <> B ].

 

/*** Commutativity of /\, \/ ***/

sets(38):       (X \/ Y) may_be_replaced_by (Y \/ X).

sets(39):       (X /\ Y) may_be_replaced_by (Y /\ X).

 

/*** Associativity of /\, \/ ***/

sets(40):       (X \/ (Y \/ Z)) & ((X \/ Y) \/ Z) are_interchangeable.

sets(41):       (X /\ (Y /\ Z)) & ((X /\ Y) /\ Z) are_interchangeable.

 

/*** Distributivity of /\, \/ ***/

sets(42):       (X /\ (Y \/ Z)) & ((X /\ Y) \/ (X /\ Z)) are_interchangeable.

sets(43):       (X \/ (Y /\ Z)) & ((X \/ Y) /\ (X \/ Z)) are_interchangeable.

 


4.16          SPECIAL.RUL

%-------------------------------------------------------------------------------

%  (C) Altran Praxis Limited

%-------------------------------------------------------------------------------

%

%  The SPARK toolset is free software; you can redistribute it and/or modify it

%  under terms of the GNU General Public License as published by the Free

%  Software Foundation; either version 3, or (at your option) any later

%  version. The SPARK toolset is distributed in the hope that it will be

%  useful, but WITHOUT ANY WARRANTY; without even the implied warranty of

%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General

%  Public License for more details. You should have received a copy of the GNU

%  General Public License distributed with the SPARK toolset; see file

%  COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of

%  the license.

%

%===============================================================================

 

%-------------------------------------------------------------------------------

% RULE FAMILIES CONTAINED HEREIN :-

%

% inference       : simple inference rules (useful for subgoaling)

% eq              : equality substitution rule

% equiv           : equivalence substitution rule

% simplify        : simplification of expressions rule

% logic           : truth-table logic rules

% standardisation : standardisation rules

% unification     : top-level unification rules

%-------------------------------------------------------------------------------

% MODEL DECLARATIONS FOR THIS FILE :-

%

% rule_family inference:

%         X       requires [ X:any        ] &

%         X or Y  requires [ X:any, Y:any ] &

%         X and Y requires [ X:any, Y:any ] &

%         X -> Y  requires [ X:any, Y:any ] &

%         X <-> Y requires [ X:any, Y:any ].

%

% rule_family eq:

%         X requires [ X:any ].

%

% rule_family equiv:

%         X requires [ X:any ].

%

% rule_family simplify:

%         X requires [ X:any ].

%

% rule_family logic:

%         X requires [ X:any ].

%

% rule_family standardisation:

%         X requires [ X:any ].

%

% rule_family unification:

%         X requires [ X:any ].

%-------------------------------------------------------------------------------

/*** Standard INFERENCE Rules ***/

inference(1): X       may_be_deduced_from [ X ].

inference(2): X       may_be_deduced_from [ Y -> X, Y ].

inference(3): X or Y  may_be_deduced_from [ X ].

inference(4): X or Y  may_be_deduced_from [ Y ].

inference(5): X and Y may_be_deduced_from [ X, Y ].

inference(6): X -> Y  may_be_deduced_from [ not X ].

inference(7): X -> Y  may_be_deduced_from [ Y ].

inference(8): X <-> Y may_be_deduced_from [ X -> Y, Y -> X ].

 

/*** SUBSTITUTION rule for equality-substitution ***/

eq(1):    X may_be_replaced_by Y if [ X=Y, goal(X\=Y) ].

 

/*** SUBSTITUTION rule for equivalence-substitution ***/

EQUIV1:   X may_be_replaced_by Y if

                [ goal(nonvar(EQUIV1)),

                  goal(EQUIV1=equiv(1)),

                  X <-> Y,

                  goal(X\=Y) ].

 

/*** SIMPLIFY rule for simplification of expressions ***/

SIMPLIFY1:    X may_be_replaced_by Y if

                [ goal(nonvar(SIMPLIFY1)),

                  goal(SIMPLIFY1=simplify(1)),

                  goal(var(Y)),

                  goal(simplify(X, Y)),

                  goal(X \= Y) ].

SIMPLIFY2:    X may_be_replaced_by Y if

                [ goal(nonvar(SIMPLIFY2)),

                  goal(SIMPLIFY2=simplify(2)),

                  goal(novars(Y)),

                  goal(X \= Y),

                  goal(simplify(X, Z)),

                  goal(simplify(Y, Z)) ].

 

/*** LOGICAL DEDUCTION rule - only allowed by explicit call ***/

LOGIC1:     X may_be_deduced_from

                [ goal(nonvar(LOGIC1)),

                  goal(LOGIC1=logic(1)),

                  goal(try_deduce(X)) ].

LOGIC2:     X may_be_replaced_by Y if

                [ goal(nonvar(LOGIC2)),

                  goal(LOGIC2=logic(2)),

                  goal(novars(Y)),

                  goal(checktype(X,boolean)),

                  goal(try_deduce(X <-> Y)) ].

 

/*** STANDARDISATION rule - only allowed by explicit call ***/

STAND1:     X may_be_replaced_by Y if

                [ goal(nonvar(STAND1)),

                  goal(STAND1=standardisation(1)),

                  goal(novars(Y)),

                  goal(X\=Y),

                  goal(checktype(X,T)),

                  goal(norm_typed_expr(X,T,Z)),

                  goal(norm_typed_expr(Y,T,Z)) ].

STAND2:     X may_be_replaced_by Y if

                [ goal(nonvar(STAND2)),

                  goal(STAND2=standardisation(2)),

                  goal(var(Y)),

                  goal(checktype(X,T)),

                  goal(norm_typed_expr(X,T,Y)) ].

STAND3:     X may_be_deduced_from

                [ goal(nonvar(STAND3)),

                  goal(STAND3=standardisation(3)),

                  goal(norm_typed_expr(X,boolean,true)) ].

 

/*** UNIFICATION rules - only allowed by explicit call ***/

/* This rule family allows f(x1,...,xn)=f(y1,...,yn) to be deduced from

   x1=y1, ..., xn=yn (for n in 1..9).  unification(n) is for the case when

   f takes n arguments.  For any n, you can survive without these rules if

   you wish: simply prove f(x1,...,xn)=f(y1,...,yn) by contradiction, then

   establish contradiction by replacing each yi by xi (or vice versa), thereby

   gaining the hypothesis f(x1,...,xn)<>f(x1,...,xn), which gives false. */

UNIF1:     X = Y may_be_deduced_from

                [ goal(nonvar(UNIF1)),

                  goal(UNIF1=unification(1)),

                  goal(X =.. [F|X1]),

                  goal(Y =.. [F|Y1]),

                  X1 = Y1 ].

UNIF2:     X = Y may_be_deduced_from

                [ goal(nonvar(UNIF2)),

                  goal(UNIF2=unification(2)),

                  goal(X =.. [F|X1,X2]),

                  goal(Y =.. [F|Y1,Y2]),

                  X1 = Y1, X2 = Y2 ].

UNIF3:     X = Y may_be_deduced_from

                [ goal(nonvar(UNIF3)),

                  goal(UNIF3=unification(3)),

                  goal(X =.. [F|X1,X2,X3]),

                  goal(Y =.. [F|Y1,Y2,Y3]),

                  X1 = Y1, X2 = Y2, X3 = Y3 ].

UNIF4:     X = Y may_be_deduced_from

                [ goal(nonvar(UNIF4)),

                  goal(UNIF4=unification(4)),

                  goal(X =.. [F|X1,X2,X3,X4]),

                  goal(Y =.. [F|Y1,Y2,Y3,Y4]),

                  X1 = Y1, X2 = Y2, X3 = Y3, X4 = Y4 ].

UNIF5:     X = Y may_be_deduced_from

                [ goal(nonvar(UNIF5)),

                  goal(UNIF5=unification(5)),

                  goal(X =.. [F|X1,X2,X3,X4,X5]),

                  goal(Y =.. [F|Y1,Y2,Y3,Y4,Y5]),

                  X1 = Y1, X2 = Y2, X3 = Y3, X4 = Y4, X5 = Y5 ].

UNIF6:     X = Y may_be_deduced_from

                [ goal(nonvar(UNIF6)),

                  goal(UNIF6=unification(6)),

                  goal(X =.. [F|X1,X2,X3,X4,X5,X6]),

                  goal(Y =.. [F|Y1,Y2,Y3,Y4,Y5,Y6]),

                  X1 = Y1, X2 = Y2, X3 = Y3, X4 = Y4, X5 = Y5, X6 = Y6 ].

UNIF7:     X = Y may_be_deduced_from

                [ goal(nonvar(UNIF7)),

                  goal(UNIF7=unification(7)),

                  goal(X =.. [F|X1,X2,X3,X4,X5,X6,X7]),

                  goal(Y =.. [F|Y1,Y2,Y3,Y4,Y5,Y6,Y7]),

                  X1=Y1, X2=Y2, X3=Y3, X4=Y4, X5=Y5, X6=Y6, X7=Y7 ].

UNIF8:     X = Y may_be_deduced_from

                [ goal(nonvar(UNIF8)),

                  goal(UNIF8=unification(8)),

                  goal(X =.. [F|X1,X2,X3,X4,X5,X6,X7,X8]),

                  goal(Y =.. [F|Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8]),

                  X1=Y1, X2=Y2, X3=Y3, X4=Y4, X5=Y5, X6=Y6, X7=Y7, X8=Y8 ].

UNIF9:     X = Y may_be_deduced_from

                [ goal(nonvar(UNIF9)),

                  goal(UNIF9=unification(9)),

                  goal(X =.. [F|X1,X2,X3,X4,X5,X6,X7,X8,X9]),

                  goal(Y =.. [F|Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9]),

                  X1=Y1,X2=Y2,X3=Y3,X4=Y4,X5=Y5,X6=Y6,X7=Y7,X8=Y8,X9=Y9 ].

 

5                       Proof Rule Syntax

The Checker supports two different types of rule, stored as databases of rules in a collection of rule files.  The two types of rule are inference rules and substitution (or “rewrite”) rules.  The inference rules allow the user to combine zero or more existing facts to infer new facts, while the replacement rules allow the user to replace a subexpression of the VC by an equivalent subexpression.  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, e.g. (A and B) may be replaced by A if the condition B=true is satisfied, so B=true is a (sufficient, but not necessary) condition for the equivalence to hold.  Some of the facts (or conditions), for either type of rule, may be “meta-logical” in that they refer to type-checking constraints or other external 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 and outlined in chapter 2 of the SPADE FDL Manual.

5.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 “)”

family-name = prolog-atom

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-prolog-expression

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

We discuss the list of conditions in section 5.3.  The rulename, the syntax of which is the same for substitution rules also, allows the user to select a family of possible rules or an individual member of a family of rules or a range of elements of a family of rules when attempting to apply a rule.  The names selected for user-defined rules should be chosen as convenient, but it is preferable to avoid using the names used in the built-in rules databases; these are listed and described in chapters 2 and 3.

The formula, as a well-formed Prolog expression, may contain Prolog variables; indeed, this is the norm: a rule without Prolog variables is rare, and is 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 FDL text 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.

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 the Prolog variables to specific values.  For example, the (hypothetical) inference rule

logic(1): A or B may_be_deduced_from [ B ].

may be used to infer (a>1 or b=2) from the fact that b=2.  The Checker requires that all Prolog variables in the formula to be inferred be fully instantiated if the rule application is to succeed, so no Prolog variables may be introduced into a VC via the use of the rules databases.  (N.B. The above rule is present in the built-in rules as inference(4) in SPECIAL.RUL.)

5.2               Substitution Rules

Substitution rules allow one subexpression of a VC to be replaced by another, equivalent, expression.  There are two types of substitution 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.

replacement-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-prolog-expression

As one would expect, one-way rules allow substitution one way round, whereas two-way rules allow interchange either way.  Thus, the rules

subst(1): A may_be_replaced_by B if [ C1, C2, ..., Cn ].

and

subst(2): A & B are_interchangeable if [ C1, C2, ..., Cn ].

both allow A to be replaced by B provided the conditions [C1,...,Cn] are met; but only subst(2) allows us to substitute the other way, i.e. replacing B by A instead.  One-way rules can be useful in preventing extra work for the Checker in symmetric rules and in directing the flow of substitutions to move towards greater simplicity.  For example, the built-in rule

commut(1): A+B may_be_replaced_by B+A.

is best expressed this way, as the two-way version of this rule says the same thing twice, and would consequently cause the Checker possibly to find twice as many matches, making the rule search longer and slower.  As an illustration of directing the flow of substitutions, consider the (hypothetical) rule

zero(1): A+0 may_be_replaced_by A.

(N.B. The above rule is present in the built-in rules, as arith(3).)  It is imaginable that, in some circumstances, we may wish to replace A by A+0; however, in general the substitution will be the other way round, as suggested by the rule.  In the rare event that we do wish to use the rule the other way round, we can still do so indirectly by inferring that A+0=A+0, then using rule zero(1) to replace one instance of A+0 in this by A to get A+0=A.  We can then use equality substitution with this fact to replace A by A+0 in the desired place.  Thus, one-way rules do not strictly affect the actual power of a proof rule, but merely suggest a particular common mode of use.

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.

5.3               Condition Lists

The list of conditions associated with a rule is a list of zero or more Prolog expressions, each of which must be “satisfied” before the rule may be fully used.  In the case of inference rules, if some, but not all of the conditions are satisfied, the rule may be used to generate subgoals to be worked on, the satisfaction of all of which allows the rule to be used.  Such subgoaling may only be used, however, when none of the unsatisfied conditions is an “immediate” condition, and when all of the unsatisfied conditions are fully instantiated.  (Please note that subgoaling cannot at present be used with substitution rules, so inference rules can be preferable on occasion.)

The conditions in a condition list are of two kinds, and the kind of the condition determines how it is to be satisfied.  The two kinds are known as ordinary conditions and immediate conditions.  Ordinary conditions are simply conditions which must follow from the hypotheses of the VC and/or from simple facts (such as 2>1).  The Checker has a built-in inference mechanism which attempts to satisfy such conditions, and the success or failure of the Checker in attempting to satisfy such a condition depends on the available hypotheses of the VC and the power of the inference mechanism; failure to satisfy an ordinary condition does not mean it is false: only that it may be, or that the Checker cannot infer it at present without further strengthening of the VC (e.g. by the user inferring intermediate useful hypotheses, for instance).

Immediate conditions are satisfied in a different way.  They take the form

goal( CONDITION )

where CONDITION is a well-formed Prolog expression.  A condition such as this succeeds if and only if CONDITION, submitted to the Prolog system as a goal with the built-in call(_) predicate, succeeds.  Thus, such conditions may call built-in Prolog code to perform some checking, simplification or action.  These immediate goals do not make any use of the Checker’s inference mechanisms, but call Prolog predicates directly.  An example of such a goal is

eq(1): A may_be_replaced_by B if [ A=B, goal(A\=B) ].

which allows A to be replaced by B provided A=B can be inferred from the VC, but only if A and B are not identical structures: the direct call to the built-in \= predicate ensures (since A and B are fully instantiated by this point, as subgoal satisfaction proceeds from left to right through the list of conditions) that A and B are distinct structures.  Without this additional immediate condition, the rule would allow us to substitute A for itself (a harmless, but pointless, substitution).

The next section lists the useful built-in predicates which may be used as immediate conditions in condition lists: no other predicates may be used apart from these, and an attempt to do so will result in a warning message when a rulefile containing an illegal predicate is read by the Checker and the Checker will then refuse to use this rule.

5.4               Permissible Immediate Condition Predicates

The following predicates may be used as immediate conditions in user-defined proof rules for use with the Proof Checker.  As well as using them directly, we may also use them with the standard combinator predicates

“_ , _”    (and)

“_ ; _”    (or).

checktype(EXPRESSION, TYPE_IDENTIFIER)

This predicate may be used to check that an expression is of an appropriate type, e.g. checktype(A,integer) before allowing A to be replaced by A+0.

EXPR1 = EXPR2

This form of equality tests for exact unifiability, so it is much stricter than equality in an ordinary goal.  For example, the ordinary goal

3+1=4

will succeed, but the immediate goal

goal(3+1=4)

will not, as 3+1 and 4 are different objects.

EXPR1 \= EXPR2

This predicate succeeds as long as EXPR1 and EXPR2 cannot be unified.  It is thus convenient for ensuring that two objects are distinct.

integer(EXPRESSION)

This built-in Prolog predicate succeeds if and only if its argument is instantiated to an integer.

intexp(EXPRESSION)

This predicate succeeds if and only if its argument is an expression composed entirely of integers (not constant- and variable-identifiers of type integer) and the built-in operators +, - (unary and binary), *, div and mod.

simplify(INPUT_EXPR, OUTPUT_EXPR)

This predicate carries out some limited simplification on an expression.  An example rule, using this and the previous predicate, is:

simpint(1): X>Y may_be_deduced_from

           [ goal( intexp(X-Y), simplify(X>Y,true) ) ].

is_in(ELEMENT, LIST)

This predicate succeeds if ELEMENT is an element of list LIST.  This predicate will not be resatisfied on backtracking.

length(LIST, LENGTH)

This built-in predicate returns the length of a well-formed list.

append(LIST1, LIST2, LIST3)

This predicate succeeds if LIST1 can be appended to the front of LIST2 to give LIST3.  It cannot be resatisfied on backtracking, so it cannot be used to do the inverse, i.e. generate pairs of lists which join together to give the third.

enumeration_list(ELEMENT, LIST)

This predicate succeeds if ELEMENT is an atom which is a constant within an enumeration type in which case the list of enumeration constants of which it is a member is returned as LIST.  It is again a “succeed once or not at all” predicate.  An example of its use might be:

enum(3): succ(pred(X))=X may_be_deduced_from

    [ goal(enumeration_list(X,L)),

      goal(L\=[X|_]) ].

sublist(LIST1, LIST2)

This predicate succeeds if LIST1 is a sublist of LIST2; it is again a “succeed once or not at all” predicate.  An example of its use might be:

enum(17):  succ(Y) may_be_replaced_by X if

    [ goal(enumeration_list(Y,L)),

      goal(sublist([Y,X],L)) ].

last(LIST, ELEMENT)

Given a list LIST, last returns the last element of the list as ELEMENT (or checks that a given value for ELEMENT is indeed the last element of LIST).  It can only succeed at most once.  To illustrate its use:

enum(1):   pred(succ(X))=X may_be_deduced_from

    [ goal(enumeration_list(X,L)),

      goal(not last(L,X)) ].

in_order(EL1, EL2, LIST)

Given a list LIST and two elements EL1 and EL2 of this list, in_order succeeds if and only if either EL1 precedes EL2 in LIST or EL1 and EL2 are equal, e.g.

enum(5):   X <= Y may_be_deduced_from

    [ goal(enumeration_list(X,L)),

      goal(in_order(X,Y,L)) ].

genvar(ATOM, VARIABLE)

This predicate should be used when you wish to include quantified expressions within proof rules (see section 5.5 below).  You should give a Prolog atom as the first argument, this being the “root” variable name, i.e. the variable name you wish to use as the bound variable of a quantified expression assuming it is o.k. to do so: if this variable is not a program identifier, the second argument, VARIABLE, is instantiated to it; if, however, the identifier is already in use, a new unique identifier based on the atom that you gave as first argument is generated to avoid any problems.  Thus, for example, goal(genvar(i,I)) will return either I=i, or I=i1 or I=i2 etc.

5.5               Quantifiers In Proof Rules

If we wish to introduce a quantified expression via a proof rule, to ensure correctness we should use the immediate goal genvar(_,_) described in section 5.4 above to generate a new unique bound variable name so that we are certain that we are not accidentally binding any occurrences of existing variables by mistake.  Thus, a rule such as

positive_array(1): all_positive(A) may_be_deduced_from

                  [ for_all(i:integer,

                       (1 <= i and i <= maxindex) ->

                          element(a, [i]) > 0) ].

should, for certain correctness (avoiding confusion with any program identifier i) be written as

positive_array(1): all_positive(A) may_be_deduced_from

                  [ goal(genvar(i,I)),

                    for_all(I:integer,

                       (1 <= I and I <= maxindex) ->

                          element(a, [I]) > 0) ].

5.6               Rule Family Declarations

Finally, in any rule file, it is necessary to declare each rule family and to provide a very basic declaration of the types of its arguments.  The rule family declaration has the form

rule_family FAMILYNAME : EXPRN1 requires TYPES1 & ...

                                & EXPRNn requires TYPESn.

(for some n >= 1).  Each different type of expression EXPRNi requires a clause in the rule family declaration.  What are these EXPRNi?  Well, for an inference rule, such as

some_rule(1): f(A1,A2,...,An) may_be_deduced_from
                  CONDITIONS.

f(X1,X2,...,Xn) (where each Xi is a different Prolog variable) is the most general form of the expression f(A1,A2,...,An), where each Ai may be a variable or other pattern.  Substitution rules come in two varieties; for a one-way rule, such as

some_rule(2): f(A1,...,An) may_be_replaced_by

                  g(B1,...,Bm) if CONDITIONS.

the only expression we need worry about is f(A1,...,An).  For a two-way rule, however, such as

some_rule(3): f(A1,...,An) & g(B1,...,Bm)
                  are_interchangeable if CONDITIONS.

we must address both f(X1,...,Xn) and g(Y1,...,Ym) (assuming f and g are different).  Remember, in all these cases, we are only concerned with the main operator or function of the expression: for all of the rules

silly_rule(1): A+B = C+D may_be_deduced_from

                  [ A+B>=C+D, A+B<=C+D ].

silly_rule(2): A-B = C   may_be_deduced_from

            [ B=0, not A<>C ].

silly_rule(3): A   = B*C may_be_deduced_from

            [ B*C=A or X, not X ].

the “most general expression” with the same main operator (in this case, =) is X=Y.  (Remember, we are only looking at the expression to be inferred or, for substitution rules, the expression(s) to be replaced.)  Note that, if we have a substitution rule in which one of the expressions to be considered is a Prolog variable, e.g.

silly_rule(4): X+Y & Z are_interchangeable if [ X+Y=Z ].

we must give a declaration for it (in this case, Z requires [Z:ir] would be appropriate, since Z must be numeric to be equal to X+Y).  Such variable declarations (i.e. where there is no main operator or function) should come at the end of your rule family declaration, otherwise they may make some of your other rules inaccessible.  Preferably, you should try to isolate such rules in a separate, type-compatible family.

If a rule family contains substitution rules which we wish to be able to use with the infer command (with the use_subst_rules_for_equality flag set to on), we must ensure that an appropriate clause of the form

A = B requires [ A:x, B:x ]

where x is i, ir, e, ire or any as appropriate.  Such a clause may already be present if there are also equality inference rules (or rules allowing expressions of the form A=B to be rewritten to something else), but if there are none, it must be included as otherwise the Proof Checker will not search this rule family for matches when asked to infer an equality.  Thus, by inclusion (or exclusion) of such a clause, one can affect whether substitution rules within a rule family may be used for equality inferences when the use_subst_rules_for_equality flag is on.

Finally, also note that, in the case of constants, we still have an expression, i.e. from

const_rule(1): max_index may_be_replaced_by 100.

const_rule(2): upper_bound & 200 are_interchangeable.

we get three expressions (max_index, upper_bound and 200: not 100, as the first rule is one-way only), each of which is its own “most general expression”.

To declare a rule family, we must first determine the collection of all such most general expressions.  Each will have N Prolog variables in it, where N is the “arity” of the main operator or function.  (The “arity” is the number of arguments, e.g. the arity of * is 2, of the built-in abs function 1, of a constant 0.)  Thus, we only need one most general expression for each different operator or function.  (In this context, the unary minus (-X) and binary minus (X-Y) operators are different.)

Having established this collection, we must next determine the permissible type of each Prolog variable in the expression.  For example, if we are writing a rule which permits X+Y to be replaced by Y+X, both X and Y may be either integer or real: it doesn’t matter which.  On the other hand, a rule which allows us to infer X>=Y+1 from X>Y is only valid if both X and Y are integers.  The permissible type does not need to distinguish between subrange types, sets and sequences etc.: most FDL types are easily distinguished by context.  It is only with integers, reals and enumerated types that we need to make a distinction (since all use the relational operators <=, >=, < and >).  We have the following type classifications available to us:

                   i                must be integer only: real but not integer is not sufficient.

                   ir              must be integer or real (i.e. numeric).

                   e                must be of an enumerated type (i.e. non-numeric).

                   ire           any ordered type (i.e. integer, real or enumerated).

                   any           all other types (e.g. boolean, set, sequence, record, array).

Because of the need from time to time to restrict arguments of rules to one of these classes, it is important that you do not mix types within a rule family in a particular file too much.  For example, the rule (mentioned earlier)

some_inequality(1): X >= Y+1 may_be_deduced_from
           [ X > Y ].

requires that both arguments of the >= operator should be in category i (integer only), whereas

some_inequality(2): X >= Y+Z may_be_deduced_from

           [ X >= Y, Z <= 0 ].

only requires that both arguments to the >= be in ir (numeric — not ire, as we use addition, which is not defined for enumerated types), and

some_inequality(3): X >= Z may_be_deduced_from
           [ X >= Y, Y >= Z ].

is o.k. for both arguments to the >= in ire (i.e. ir or e).  Given this, it would be wise to put these three rules into three distinct families (or in three distinct files, or both).  If we put them into the same family, we must declare

rule family some_inequality: A >= B requires [ A:i, B:i ].

as otherwise, the first rule might be used with arguments which are real but not integer, in which case this rule would be invalid.

For each different most general expression occurring within a family, you should provide a single declaration in which each Prolog variable in each declared expression is given a classification.  The classification list (following the keyword requires) is zero or more matches of the form VARIABLE:CLASSIFICATION (where VARIABLE is the Prolog variable whose classification is being declared and CLASSIFICATION is one of i, ir, e, ire or any), separated by commas.  In the case of constants, the classification list is the empty list [].

To give you a feel for the declarations necessary, all of the Proof Checker’s built-in rule files contain (as comments) the rule family declarations which would be needed if these rule files were not built-in (see chapter 4).  Finally, note that a rule family’s declaration must precede the rule family in the rule file.

5.7               Comments In Rule Files

As the Proof Checker is written in Prolog, comments within rule files should be delimited by the /* and */ character sequences.

We strongly recommend that you should use comments freely within proof rule files, for instance to provide justifications for the rules, to give precise definitions of proof functions from which the rules are claimed to follow and to record any changes made to the rulefile.

6                       Definition And Proof Of Proof Rules

In the previous chapter, we considered the syntax of user-definable proof rules.  In this chapter, we give some advice on ensuring that the proof rules introduced to the Proof Checker in this way are “sensible”: non-contradictory and based on a precise definition of the functions involved.  The main problem arises when one introduces one or more proof rules which are intended to capture the semantics of a proof function introduced in code annotations: are the conditions in the proof rules strong enough?  Have all cases been covered?  What is the true domain of the function?  How can we prove that a collection of rules follow from a definition of a function?  These are concerns which we address here.

In section 6.1 we consider the notion of a definition of a function and consider explicit and implicit definitions and the coverage of the function domain.  In section 6.2 we consider what we mean by properties, and how we might go about proving, perhaps only semi-formally, that a property follows from some definitions.  In section 6.3 we discuss issues to do with the domains of functions and what we can do to guard against definedness problems when employing “partial” functions.  Finally, in section 6.4 we consider how we can use the SPADE Proof Checker to support the type of proof-work which might arise in section 6.2 — that property rules follow from definitions — and illustrate this with an example.

6.1               Definitions

6.1.1           Introduction

We assume that the reader is familiar with the notion of a mathematical function as something which, for particular argument values, returns a particular result value.  Thus, abs(_) is a built-in FDL function which, when applied to the argument -3 returns 3.  Note that abs(_) cannot return any other value when applied to -3: for every possible argument value, abs(_) can return at most one value, because it is a function (rather than a relation).  However, there is more than one argument value which, when used as argument to abs(_), returns the result 3: both abs(-3) and abs(3) return 3 for instance.  Equally, there are “result values” (in the type integer) for which no argument to abs(_) exists which returns such a value: e.g. abs(x) = -1 is impossible for any x.  We can make all of these statements with confidence because we can state a definition for abs (whose signature we regard here as integer --> integer, ignoring for the moment its use with real arguments also):

abs(x)     == x   if x >= 0,

           == -x  if x < 0

(here, == should be read as “equals by definition”) and from this prove theorems:

for_all(x:integer, for_some(y:integer, abs(x) = y))

for_some(x:integer, for_some(y:integer,

                                abs(x) = abs(y) and x <> y))

for_some(x:integer, for_all(y:integer, abs(y) <> x)).

The first theorem reassures us that the function abs(_) is fully defined over the whole of the candidate domain integer: we can apply abs(_) to any integer and we will always get a result.  (In other words, abs(_) is not partial with respect to the domain integer).  The second theorem demonstrates that abs(_) is not one-to-one (since two different arguments may map to the same result) and the third theorem demonstrates that abs(_) is not onto (i.e. there exist elements in the range integer to which no argument value ever gets mapped).

In defining a function for use with the Checker, it is necessary first of all to give a signature (in the FDL text) giving the types of the function’s argument(s) and the type of its result.  We call the cartesian product of the argument types (regarded as sets) the domain of the function and the result type its range.  However, in this, any subtype (e.g. a subrange of the integers, or a subrange of an enumerated type) is regarded as its base type, so type smallint = 0..255 is regarded as the type integer, which is the unbounded set of integers.  With this extension (which gives us static typechecking), we call the function a total function if it is properly defined for every possible element of the domain, and a partial function if it is only defined for a subset of this general domain.  For partial functions, we should also ensure that we are applying the function to elements of the true domain (i.e. the subset of the domain over which the function is properly defined), using techniques which we shall discuss in section 6.3.

6.1.2           Explicit Definitions

By far the most straightforward means of defining a function is through an explicit definition.  An explicit definition of a function f takes the form

f(x1,...,xn)      = a1(x1,...,xn)      if p1(x1,...,xn),

                  = a2(x1,...,xn)      if p2(x1,...,xn),

                  ..........

                  = am(x1,...,xn)      if pm(x1,...,xn).

In this definition, each ai is a function (hopefully simpler!) which applies when the predicate pi is true.  It is important that the pi are disjoint, i.e. that for each possible (x1,...,xn) in the domain of f, at most one pi holds, since otherwise the definition may be self-contradictory; we should only ever relax this requirement if we can prove that all possible overlaps always give precisely the same results.  If it is also the case that at least one pi holds, then f is a total function over this domain (provided each of the ai is suitably total over the required domains when pi is true).  Thus, our example definition of abs(_) restricted to the integers in the preceding subsection is an explicit definition (it has the above form) and it is total, since for any integer x, it must satisfy one and only one of the predicates {x>=0, x<0}.  With such explicit definitions, it can be straightforward to identify parts of the domain for which the function is not defined (because none of the pi cover this case, or because some of the ai are themselves partial over parts of the domain for which they are used).  Note that there is an implicit universal quantification over the x1,...,xn in such explicit definitions.

6.1.3           Implicit Definitions

Implicit definitions may be more difficult to use and to check for definedness than explicit ones.  If we are lucky, it may be possible to rewrite them into an implicit form, e.g. if we regard

for_all(x:integer, for_all(y:integer,

           y <> 0 -> (x div y) * y + x mod y = x))

as an implicit definition of mod (in terms of div, * and +) we can rewrite the equality to yield

for_all(x:integer, for_all(y:integer,

    y <> 0 -> x mod y = x - (x div y) * y))

and use this for our definition of the (partial) function mod, since subtraction is available to us as the inverse to addition.  However, for the more general case where we have

for_all(x1:t1, ..., for_all(xn:tn,

        p(x1,...,xn,f(x1,...,xn)) )...)

as an implicit definition of f, it may not be so easy!  If you think that (for function sr (integer): integer)

for_all(x:integer, sr(x) * sr(x) = x)

is a reasonable definition of a square root function, for instance, think again: first, is sr returning the positive or the negative square root (or will it sometimes return one, sometimes the other according to the value of x)?  Secondly, when is sr undefined?  (It is clearly partial, since no (non-imaginary) value when multiplied by itself gives -1 for instance, and no integer value squared gives 2.  Are these the only problem values?  Just think how much more difficult it is to decide this for less simple implicit definitions!)

Where implicit definitions do arise (as a result of their use in the routine’s specification for instance), concerns over definedness and determinism are more complex and will need to be thought about individually.  However, there is a class of implicit definitions which can be handled more easily, to which we turn our attention next.

6.1.4           Recursive Definitions

A recursive definition defines a function in terms of a number of base cases and a number of recursion cases.  Thus, the simple example

for_all(n: integer,

    {1}    (n = 0 -> factorial(n) = 1) and

    {2}    (n > 0 -> factorial(n) = n * factorial(n-1)))

can be seen to be a reasonable recursive definition of the function factorial for all non-negative integers, since every possible non-negative integer argument to factorial will be covered by a number of applications of the second (recursion case) defining property followed by an application of the first (base case) property.  In making this observation, we are effectively reasoning that the definition is well-formed by mathematical induction.  Where we can come up with effective inductive arguments as to the definedness of such recursively-defined functions, we may be satisfied with our definition, though we must be careful that the base cases are sufficient to ensure termination in all cases of interest, and we should beware that the definition is sufficiently unambiguous for our purposes.  As another example of a reasonable recursive definition, consider

type intseq = sequence of integer;

function sum_seq (intseq): integer;

for_all(s:intseq,

    {1}    (s = [] -> sum_seq(s) = 0) and

    {2}    (s <> [] -> sum_seq(s) = first(s) +

                  sum_seq(nonfirst(s)))).

This recursively defines a function which sums the elements of a sequence of integers, regarding the empty-list as having sum zero.

6.2               Properties

Typically, in a file of proof rules we may be more interested in giving particular properties of the functions which we have defined, rather than merely giving the definition repeatedly using this.  For example, we may define a predicate

ordered(a, l, u) ==

    for_all(i:integer, (l <= i and i < u) -> a[i] <= a[i+1])

which is true whenever array a is ordered over the range l..u.  From this, we can make a number of observations, thus (all implicitly universally quantified):

l > u -> ordered(a, l, u)

ordered(a, l, l)

ordered(a, l, m) and ordered(a, m, u) -> ordered(a, l, u)

ordered(a, l, u) and a[u] <= a[u+1] -> ordered(a, l, u+1)

These observations may be more useful in proving the correctness of a sort algorithm than the strict definition above: ordered(a, l, l) may be of use for the initialisation path from the start of the routine to the (presumable) code loop(s) and the fourth property might be of use in proving the correctness of paths around the loop, for instance.

It is all very well to state these properties, but how do we ensure that they are not self-contradictory and that they capture all the required detail? (My first instinct was to write the third property above as

ordered(a, l, m) and ordered(a, m+1, u) -> ordered(a, l, u)

for instance, but this allows a[m] to be greater than a[m+1]: not a very satisfactory concept of ordering!)  If we have not given a proper definition of the function, the answer may be: very little.  If, however, we have given a strict definition (and, better still, this definition is explicit and total), we may use this definition to prove that the required properties are indeed consequences of it.  For instance, let’s outline a proof of (the correct form of) property three above.  As the definition of ordered is a single clause, it always applies (there are no distinct options to consider by cases).  Thus, we can expand property three out to yield

H1:  for_all(i:integer, (l <= i and i < m) -> a[i] <=
           a[i+1])

H2:  for_all(i:integer, (m <= i and i < u) -> a[i] <=
           a[i+1])

-->

  C1:  for_all(i:integer, (l <= i and i < u) -> a[i]
           <= a[i+1]).

(Here, I have rewritten the formula (A and B -> C), making C the conclusion C1, and A and B hypotheses H1 and H2 respectively, arriving at a form more reminiscent of Proof Checker formulae.)  How do we prove the conclusion for all i in l..u-1?  By cases: either i is in l..m-1, or i is in m..u-1.  In the first case, we can use H1 to prove that a[i] <= a[i+1].  For case 2, i is in m..u-1, so we may now use H2 to prove the conclusion.  Either way, the conclusion holds so we have proved C1 by cases.  (Why does this not work for the erroneous property three given earlier? -- Try it!)

Thus, where we have an adequate definition, we can use this to prove properties and then utilise these properties as proof rules.  In fact, we can perform the proofs that the properties follow from the definition using the Proof Checker, if we have restricted ourselves to first-order classical logic, as we shall consider in section 6.4.  First, in the next section, we turn to a question which may have occurred to you in reading the above: what happens when the array indices go out of range in this argument?

6.3               Partiality

A classic example of a partial function is the integer division operator, div; this only has a value if its second argument is non-zero.  However, in most conventional imperative languages, all the arithmetic operators are partial: if x+y goes outside the subrange -32768..32767 (or some other integer subrange), we get a run-time error (or odd behaviour).  We may guard against this where it is of concern to us by embedding check statements in our FDL model, e.g.

check  d <> 0;

x := c div d;

We may think this is sufficient; is it?  No!  If c=-32768, d=-1, the correct result is 32768, which is outside our subrange; with the above check, we are proving that the result of the algorithm is mathematically defined on a machine with “better” arithmetic, but we have not completely established absence of overflow/run-time error.  However, in principle it is possible to annotate our code in such a way as to establish this for most programs of interest.

If we introduce such checks, we may then establish that such subrange rules (i.e. restriction to true domain) are being respected by our algorithm.  But we must be careful to include and establish these partiality conditions in our proof annotations (pre and post and assert statements, for instance) and to maintain these in our proof rules.  Thus, in the preceding section we abstracted out of our definition of ordered the fact that the array-type object used as first argument to ordered has a valid index range outside which we should not access elements.  We have a choice as to how best to ensure that no violation arises in practice; we may either modify the definition of ordered to read

ordered(a, l, u) ==

for_all(i:integer,

               (l <= i and a_low <= i and i < u and i < a_high) ->

           a[i] <= a[i+1])

(where the index range of a is a_low..a_high) and then reflect these extra constraints in each of our proof rules about ordered, or we may add extra conditions to any assertions about ordered, e.g. augmenting

ordered(a, l, u)

to

ordered(a, l, u) and a_low <= l and l <= a_high and

a_low <= u and u <= a_high.

The choice is in part a matter of personal preference: you should choose the route which you regard as most satisfactory for your approach to proof.

6.4               Proofs Of Properties From Definitions

As we saw in section 6.2, from a definition we may establish consequences for use as proof rules.  One example was the ordered predicate; another is the predicate maxof, defined by

maxof(x,a,l,u) ==

for_all(i:integer, (l <= i and i <= u) -> a[i] <= x)
       and for_some(i:integer, l <= i and i <= u and a[i] = x)

where

const low_int = integer: pending;

const high_int = integer: pending;

type indexrange = low_int..high_int;

type arrayofint = array [indexrange] of integer;

function maxof (integer, arrayofint, indexrange,

    indexrange): boolean .

We claim that the four proof rules

max(1):  not maxof(X,A,L,U) may_be_deduced_from [ L>U ].

max(2):  maxof(element(A,[L]),A,L,L) may_be_deduced.

max(3):  maxof(X,A,L,U+1) may_be_deduced_from

           [ maxof(X,A,L,U), X >= element(A,[U+1]) ].

max(4):  maxof(element(A,[U+1]),A,L,U+1)

           may_be_deduced_from

             [ maxof(X,A,L,U), element(A,[U+1]) >= X ].

are consequences of this definition; how can we prove this using the Checker for support?

First of all, we write the definition of maxof out as a single proof rule, thus:

maxdef(1): maxof(X,A,L,U)  may_be_replaced_by

           ( for_all(i:integer,

               (L <= i and i <= U) ->

                      element(A,[i]) <= X)

           and

             for_some(i:integer,

               L <= i and i <= U and element(A,[i]) = X)

           ).

and include this as the only rule in our rule file.  Next, we create a .VCG file containing four formulae to prove, one for each of the rules to be established.  Notice that to establish inference rules, which all of the above are, we map

X may_be_deduced_from Y to     Y’ ->  X

X may_be_deduced                to     X

(where Y’ is the formula (Y1 and ... and Yn) for list [Y1,...,Yn]).  For substitution rules, we map

X may_be_replaced_by Y if Z             to     Z’ ->  X=Y

X & Y are_interchangeable if Z to     Z’ ->  X=Y

X may_be_replaced_by Y          to     X=Y

X & Y are_interchangeable               to     X=Y .

Thus, for the above four proof rules, we get a .VCG file of the form shown overleaf:


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

                       RESULTS OF SPADE SEMANTIC ANALYSIS

                           PVL SPADE TOOL VERSION : 4.3

                Program Validation Limited, Southampton, England

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

                               maxof proof rules

                     DATE : 25-DEC-1988 TIME : 00:00:00.00

                            VERIFICATION CONDITIONS

                                (not simplified)

 

For proof rule max(1) [empty-range case] :

maxof_proof_rule_1.

H1:   l > u.

      ->

C1:   not maxof(x, a, l, u).

 

For proof rule max(2) [unit-range case] :

maxof_proof_rule_2.

H1:   true.

      ->

C1:   maxof(element(a, [l]), a, l, l).

 

For proof rule max(3) [extension of range - case 1] :

maxof_proof_rule_3.

H1:   maxof(x, a, l, u).

H2:   x >= element(a, [u + 1]).

      ->

C1:   maxof(x, a, l, u + 1).

 

For proof rule max(4) [extension of range - case 2] :

maxof_proof_rule_4.

H1:   maxof(x, a, l, u).

H2:   element(a, [u + 1]) >= x.

      ->

C1:   maxof(element(a, [u + 1]), a, l, u + 1).

 

 

Figure 5(a): Formulae to establish correctness of max rules


Notice that in this .VCG file, all of the “variables” (x, a, l, u) are implicitly universally quantified.  Also, it is important to ensure that such manually-produced .VCG files are in exactly the right format: see chapter 4 of the SPADE Proof Checker User Manual for some observations on the format of .VCG files.  Finally, we also need a .FDL file declaring the objects used in the .VCG file, thus:

title maxof proof rules;

const low_int = integer: pending;

const high_int = integer: pending;

type indexrange = low_int .. high_int;

type arrayofint = array [indexrange] of integer;

proof function maxof (integer, arrayofint,

    indexrange,

    indexrange): boolean;

var a: arrayofint;

var l, u: indexrange;

var x: integer;

start

   {*** DUMMY FDL MODEL - USED FOR TYPE INFORMATION

           ONLY ***}

finish

We can then enter the Proof Checker and use the maxdef(1) proof rule to prove each of the four VCs in turn.  Where such properties of defined functions are being used, this is a worthwhile exercise, both to vet the definition and rules by exercising the former and establishing the latter as consequences and to demonstrate consistency and increase one’s familiarity with and understanding of the proof functions employed.

7                       Using Buildchlib, The Rule-Library Builder

The tool Buildchlib is no longer shipped with the Checker following the release of version 2.05.  The use of user-defined rule files is still permitted, through the consult command.  For further information contact Altran Praxis.

 

Document Control and References

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

Copyright Altran Praxis Limited 2010.  All rights reserved.

File under

$CVSROOT/userdocs/Checker_Rules.doc (was formerly S.P0468.73.32)

Changes history

Issue 0.1  (1st July 1997):  Conversion to new standard document format.

Issue 0.2  (17th December 1997):  Minor formatting changes made.

Issue 0.3  (21st January 1998):  After initial review by Ian O’Neill.

Issue 1.0  (30th January 1998):  After formal review.

Issue 2.0  (6th November 2001): Updated for release 1.46

Issue 2.1  (11th January 2002):  Included two new rulefiles.

Issue 2.2  (30th May 2002): Included ENUMERATION.RUL (CFR 1052)

Issue 3.0  (24th June 2002): Definitive issue to accompany Checker 1.47 following review S.P0468.79.77.

Issue 4.0  (2nd April 2003): Updated to new template format.

Issue 5.0  (9th June 2003):  Changes to new template, final format.

Issue 5.1 (7th June 2004): Correction to rule exp(6) in FDLFUNCS (CFR 1374)

Issue 5.2 (23rd November 2004): Changed company name only.

Issue 5.3 (1st July 2005): Updated rules following SICSTUS PROLOG Port.

Issue 5.4 (6th July 2005): Updated unification rules following CFR 1526.

Issue 5.5 (16th November 2005): Removal of buildchlib and new rule modular(32).

Issue 5.6 (22nd November 2005): Changed Line Manager.

Issue 5.7 (15th December 2005): Updated following review S.P0468.79.90.

Issue 5.8 (20th March 2006): Correction to rules intdiv(5) and intdiv(6).

Issue 5.9 (2nd February 2009): Modify copyright notice.

Issue 6.0 (17th September 2009): Update copyright and licence information in listings of proof rule files.

Issue 6.1 (3rd February 2010): Rebrand for Altran Praxis Limited

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

Changes forecast

Nil.

Document references

None.