© B-Core
(UK) Limited, Last updated: 22 Feb 2002
B-TL can be viewed as a kind of logic/functional programming language, whose program statements, called ``Theories'' consist of ordered sets of inference rules. A natural-deduction-style proof engine uses backwards and forwards inference to evaluate programs. Rewriting is treated as a special form of backwards inference.
A tactic language is used to add additional control to the inference mechanism.
B-TL is also the language used to supply additional user theories to the B-Toolkit's Animator and InterProver.
Although no explicit interface to the B-Platform is visible through the B-Toolkit, experienced B-Toolkit users will need to have knowledge of the syntax of B-TL and the proof mechanisms used in the B-Platform.
The B-Platform is best viewed as a ``Proof Assistant'' in constructing formal proofs. It is not a true ``Theorem Prover'', because inference rules supplied by the user do not have to be proved in terms of some basic set of axioms. The B-Platform just mechanises the application of rules, and assists with some of the house-keeping.
The B-Platform can be purchased separately from B-Core (UK) Ltd. in their product called the B-Tool (rather than B-Toolkit). It is useful for playing with and learning about proof, as well as for implementing advanced tools such as provers; the B-Platform is also sometimes referred to as the B-Kernel.
For the purposes of B-Toolkit users, a limited knowledge the syntax of a formula in B-TL is all that is required; other aspects of the language are not relevant. What follows below is not intended to be a thorough description of the B-Platform, or a complete syntax for B-TL, but rather a summary of those aspects that are essential to a working knowledge for the B-Toolkit user.
A Joker can be any single upper or lower-case letter. A Joker is true variable which can be replaced by any Formula. It is to be distinguished from AMN variables, which appear as identifiers in B-TL, which have to be at least two characters long.
Identifiers can be modified by appending a Number. This is to allow tools to create new variables when copying formulae. In the B-Toolkit, it is used to distinguish between copies of the same state variable in different contexts (inside and outside of a loop, for instance).
Three major types of rules are distinguished, `` simple rules'', `` rewrite rules'' and `` forward rules'', which, despite being syntactically similar, are applied in very different ways. Simple rules and rewrite rules are both used in backwards inference, and so are grouped as ``backward rules''.
Simple_Rule ::= Antecedents => Consequent | Consequent Antecedents ::= Antecedents & Formula | Formula Consequent ::= FormulaAn example of a simple rule is:-
a <: c &
b <: c
=>
a \/ b <: c
This rule states, in effect, that a goal of the form
a \/ b <: ccan be proved if the two goals
a <: b &
a <: c
can both be proved.
In this example, a, b and c are Jokers which stand for any formula. So applying this rule to the goal
STAFF \/ CUSTOMER <: PERSONhas the effect of applying the rule
STAFF <: PERSON &
CUSTOMER <: PERSON
=>
STAFF \/ CUSTOMER <: PERSON
Simple rules are used for Backwards
Inference. They are applied as follows:-
a : {a}
could match and discharge the goal
percy : {percy}
Rewrite_Rule ::= Antecedents => Rewrite | Rewrite Rewrite ::= Formula == FormulaAn example of a rewrite rule is:-
not(s = {})
=>
max({max(s),x}) == max(s\/{x})
This rule states, in effect, that, if not(s = {}) can be proved,
any sub-formula of the current goal that has the form max({max(s),x})
can be rewritten as max(s\/{x}).
The Jokers s and x can be replaced by any formula, so that applying this rule to the goal
max({max({0}),new}) == max({0}\/{new})
has the effect of applying the rule
not({0} = {})
=>
max({max({0}),new}) == max({0}\/{new})
Rewrite rules are used for Backwards
Inference, and are applied as follows:-
Forward_Rule ::= Antecedents => ConsequentAn example of a Forward Rule is :-
not(a:T) & a:(S\/T) => a:SThis rule states, in effect, that, if it is known that not(a:T) and that a:(S\/T), then it is also known that a:S.
The Jokers a, S and T can be replaced by any formula, so that applying this rule to the hypotheses
not(percy:STAFF) & percy:(CUSTOMER\/STAFF)has the effect of applying the rule
not(percy:STAFF) & percy:(CUSTOMER\/STAFF) => percy:CUSTOMERForward rules are used for Forwards Inference, which is used every time a new hypothesis is introduced into the set of hypotheses.
Forwards rules are applied as follows:-
For example, matching the formula
age(p) : Tto the formula
age(percy) : 0..120is achieved using the substitution
p , T := percy , (0..120)Special care must be taken with the matching to comma-separated lists. The comma operator is treated just like other left-associative infix operators. So the formula {p} can match the formula {1,2,3} with substitution
p := 1,2,3whereas {P,p} would match as
P , p := (1,2) , 3
Guards also provide a means of making inference rules more generic. Their syntax is as follows:
Guards ::= Guards & Guard | Guard Guard ::= "binhyp" ( Formula ) | "bnum" ( Formula ) | "bident" ( Formula ) | "bstring" ( Formula ) | "btest" ( Number Comparison Number ) | "bsearch" ( Formula , ( Formula_List ) , Formula ) | "breade" ( Formula , Formula_List , Formula ) Comparison ::= < | <= | > | >= | = | /=In this context, a Number is any Natural number less than 2^32. A Formula_List is comma (or in some cases ``&'', ``or'' or ``;'') separated list of Formulae.
A brief explanation of these guards is as follows:-
binhyp(f:S-->T) & x:S => f(x) : Tto the formula
age(pers) : 0..120in the presence of the hypothesis
age:PERSON-->0..120behaves as if the following rule is applied:-
age:PERSON-->0..120 & pers:PERSON => age(pers) : 0..120
btest(a/=b)
=>
not(a:{b})
For example, a typical use of this guard is as follows:-
bsearch((x < y),P,Q) & [x,y := 1,2]P => #(x,y).PThis rule can be used to attempt to prove an existential quantifier in which P contains the constraint x < y by selecting specific values for x and y, namely 1 and 2.
The antecedent [x,y := 1,2]P is a predicate identical to P with all free occurrences of x and y replaced by 1 and 2 respectively. So applying this rule to the goal
#(a,b).( a:NAT & b:NAT & a < b )has the same effect as applying the rule
1:NAT & 2:NAT & 1 < 2 => #(a,b).( a:NAT & b:NAT & a < b )Careful attention is, of course, given to the renaming of variables to ensure that clashes with free variables are avoided.
The format string f works on the same kind of principle as printf function in C. The % character is used to mark the position of formulas in the output, and various escape characters are allowed, such as follows:-
For example, another way of treating the existential quantification above is by providing the rule:-
breade("\n -- Choose values for %,% which satisfy % : ",x,y,P,(s,t)) &
[x,y := s,t]Q
=>
#(x,y).P
Attempted application of this rule to the goal
#(a,b).( a:NAT & b:NAT & a<b )would result in the following message being displayed on the screen:-
-- Choose values for a,b which satisfy (a:NAT & b:NAT & a<b) :to which the user may respond by typing 1,2 for the same effect of the bsearch example above.
The interactive tracing of attempted rule applications can be achieved by including antecedents of the following form:-
breade("\n *** APPLYING MY SPECIAL RULE TO % : ",(#(x,y).P),v) &
bsearch((x < y),P,Q) &
[x,y := 1,2]Q
=>
#(x,y).P
An example is:-
bident(b)
=>
{a} \/ {b} == {a,b}
Theory ::= THEORY Theory_Name IS Rule_List END Theory_Name ::= Identifier Rule_List ::= Rule_List ; Inference_Rule | Inference_RuleIn the Proof Method files presented by the user to the InterProver, backwards rules and forwards rules are presented in two theories, usually called UsersTheory and FwdUsersTheory respectively. There is no reason, however, why users should not present any number of theories with others names, as long as the appropriate tactics are also amended.
The order of rules in a theory is significant. (See Ordering Rules in Theories below for a discussion of this.)
Tactic ::= Atomic_Tactic | Tactic ; Tactic | Tactic~ Atomic_Tactic ::= DED | GEN | SUB | HYP | FEQL | Theory_NameThe semicolon indicates sequencing of actions, and the tilda indicates repetition. The following is an example of a tactic:-
( Theory1 ; DED ) ~ ; Theory2~which says, in effect:-
By default, these two tactics are presented as:-
(UsersTheory~), (FwdUsersTheory~/*;FEQL~*/)and the user is expected to present backwards rules in a theory called UsersTheory and forwards rules in FwdUsersTheory.
Note that the application of the special tactic FEQL is commented out by the annotation marks /* and */. It is placed there to remind users that a frequently desired modification of the forward tactic is to include the ``forwards equality'' tactic. In some applications, this modification helps to push proofs through, often without providing additional rules. It is left out of the default for efficiency reasons.
The special tactics are described as follows:-
H1 & H2 & ... Hn => Gby placing the formulae H1, H2 ... Hn into the current set of hypotheses, and making G the current goal.
!v.Gby renaming all the variable v in G to avoid free occurrences in the current set of hypotheses, and making the renamed G the new goal.
[v:=F]Gby performing the substitution on G, and making the rewritten goal the new goal.
P1 & P2 ... Pn => Qthe current goal Q is replaced by P1, P2 ... and Pn.
!v.Gwhere G is identical to Q for some value of v, then the current goal Q is discharged.
For example, if the set of current hypotheses contains
newperson = percy
newage = 23
age +> {newperson |-> newage} <: PERSON --> AGE
then the FEQL tactic would have the effect of expanding the set to
newperson = percy
newage = 23
age +> {newperson |-> newage} <: PERSON --> AGE
age +> {percy |-> 23} <: PERSON --> AGE
For example, consider the following theory:-
THEORY max IS
max({p}) == p
;
max({max(P)}\/Q) == max(P\/Q)
;
max({P,p}) == maxel({P,p},0)
;
maxel({p},q) == p
;
btest(q>p)
=>
maxel({p},q) == p
;
maxel({P,p},q) == maxel({P},p)
;
btest(q>p)
=>
maxel({P,p},q) == maxel({P},q)
END
The last rule is attempted first. This rule is guarded by a btest.
If this fails, then the next rule above is attempted.
The rewrite in the next rule has an identical left-hand side, so the rule will match exactly when the bottom rule does. This time, however, there is no guard, but we know from the failure of the rule below that it will only apply when q<=p.
Together, these last two rules cover all cases when there are at least two elements in the set in the first argument of maxel.
The next rule up has a rewrite with a different (more general) left-hand side. The formula {p} can match any set, including those of the form {P,p} (see Pattern Matching). But we know that, since the previous rules did not match, the only pattern that remains to be matched is the single set, in which p matches a single element, and not a comma-separated list. A similar argument applies to the top rule.
The first control over the application of a rewrite rule is through pattern matching: the rule will only apply if the shape of the left-hand side of the rewrite matches a sub-formula of the current goal.
A second level of control is by judicious ordering of rewrite rules in the theory. (See Ordering Rules in Theories above.)
A third level of control is by using guards in the antecedent of the rule: if guards evaluate to false, the rule is not applied.
A better version of the rewrite rule example given above is thus:-
binhyp(not(s = {}))
=>
max({max(s),x}) == max(s\/{x})
since this only allows rewriting when it is known from the current set
of hypotheses that
not(s = {}).
It is therefore recommended that simple rules and rewrite rules are used in preference to forwards rules where ever possible.
© B-Core
(UK) Limited, Last updated: 22 Feb 2002