if
Formulapred Fib_prev2(index :< I, prev :> I, fib :> I) iff {'fib' is the 'index'-th Fibonacci number, and prev is the one before it} if index <= 2 then fib = 1 & prev = 1 else Fib_prev2(index-1, befprev, prev) & fib = prev + befprev endThe general form of an if formula is:
Formally, the if formula is true if both the A and the B are true, or if the A is false and the C is true. However, you can think about it in terms of instructions to the system in the following way:
If the condition holds, then evaluate the then formula; otherwise, evaluate the else formula. So using an if formula of the form given above is equivalent to using(A & B) | (~A & C)where ~A expresses the opposite condition to A (for instance, index > 2 and index <=2). There is a restriction on A, the condition formula, namely that all the terms that appear there must be full value.
A is meant to be a test, not a constraint. There is no such restriction on B or C however.
Thus the following is valid and will compile properly:pred Rex (x :< L,z :: L) iff if x < 3 then z < x else z > x+12 endNormally the restriction on A is one you can live with. Often it helps to isolate your "if" in its own predicate, like pred Rex above, or its own procedure and pass it all the parameters it needs to function correctly and collect any or all calculated values as output parameters.
However, if you must use symbolic variables in A, your condition formula, then you can - directly in your predicate - embed code of the form (( A & B ) | C ) where A, B and C are formulas. Recall that this is logically equivalent to "if A then B else C end".
As an example, look at the following pseudo-code:x::L & y::L & z::L & if x < y then z >= 6 else z < x+y+2 endThis test can be expressed in FormulaOne as
(( x < y & z >= 6) | z < x+y+2 )if and its close relative case are rather deterministically oriented structures. The procedural approach to them described in the next section is often more readable and efficient.
if
pred Fib3(index :< I, fib :> I) iff {'fib' is the 'index'-th Fibonacci number} if index < 1 then Print('Warning: Fib index less than 1!') end & Fib_prev2(index, prev, fib)If you tried to program this kind of thing without an if formula, you would get something like this:
pred Fib4(index :< I, fib :> I) iff ( index < 1 & Print('Warning: Fib index less than 1!') | index >= 1 ) & Fib_prev2(index, prev, fib)Clearly, the version with the if is more understandable. You may often have several if formulas strung together by the else clauses like this:
if A then B else if C then D else if E then F .... end end endIn this case, you can use the elsif construct to make the conditions a little more readable:
if A then B elsif C then D elsif E then F endNote that only one end keyword is necessary at the end of the sequence. This makes more sense in cases where the conditions are really equal possibilities, rather than some being subordinate to others. Consider this version of the greatest-common-divisor predicate, GCD1.
pred GCD1(x :< L, y :< L, n :> L) iff {the greatest common divisor of 'x' and 'y' is 'n'} if y = 0 then n = x elsif x = 0 then n = y elsif x < y then GCD1(x, y-x, n) else GCD1(x-y, y, n) endHere's another example of an elsif predicate. We'll see a better version of this below, in the section on case formulas.
pred Digit_name(x :< [0..3], name :> S) iff {the English name of 'x' is 'name'} if x = 0 then name = 'zero' elsif x = 1 then name = 'one' elsif x = 2 then name = 'two' else name = 'three' end
pred Sum2(l :< list I, s :> I) iff {the sum of the list elements of 'l' is 's'} case l of Nil => s = 0; (head, tail) => Sum2(tail, tailsum) & s = head + tailsum endThe terms to the left of the arrows (=>) in the case formula are the various different forms l can take; and the formulas to the right of them are the conditions which must hold true, in each of those cases, for the predicate to be true. The general format of the case formula is:
Only certain types of variables can be subject terms. (Subject terms are usually going to be variables, because if the structure of the term were explicit, you would not need to know what structure it had!). Only variables of list types, integer types, string types and union types (which we'll discuss later) can be subject terms.
For example, say you wanted to write a predicate to give the English names of the digits, like the example in the last section. The following definition would work:pred Digit_name1(digit :< [0..9], name :> S) iff {'digit' has the English name 'name'} case digit of 0 => name = 'zero'; 1 => name = 'one'; 2 => name = 'two'; 3 => name = 'three'; 4 => name = 'four'; 5 => name = 'five'; 6 => name = 'six'; 7 => name = 'seven'; 8 => name = 'eight'; 9 => name = 'nine'; endHowever, if we had declared digit to be of type I, it would not have been acceptable, since the given case statement would not have covered all possible values of the variable.
FormulaOne allows two kinds of variants to the case statement which streamline them in many instances. After a list of cases, which may not cover all possible forms, there can be a final clause, just before the end, of the form else formula.
This works in the same way as the else part of a long if ... .... elsif statement. It catches all other cases not covered by the previous case terms. So if we wanted to consider all digits over 3 to be 'many', we could modify our Digit_name predicate as follows:pred Digit_name2(digit :< [0..9], name :> S) iff case digit of 0 => name = 'zero'; 1 => name = 'one'; 2 => name = 'two'; 3 => name = 'three'; else name = 'many' endThe other streamlining variant FormulaOne allows is to group more than one case term before the arrow when all their case conclusion formulas are the same. The case terms are separated by or "|" symbols.
pred Digit_name3(digit :< [0..9], name :> S) iff case digit of 0 => name = 'zero'; 1 => name = 'one'; 2 => name = 'two'; 3 => name = 'three'; 4 | 5 | 6 => name = 'several'; else name = 'many' endThe following example uses variable of string type in the subject term. Note that for string type the else clause is mandatory.
proc Beatle_name(name:<S) iff case name of 'Ringo' => Print('Starr'); 'George' => Print('Harrison'); 'Paul' => Print('McCartney'); 'John' => Print('Lennon'); else Print('Not a Beatle') end