French German Italian Spanish Portuguese Japanese Korean Chinese

The

**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 A then B else C end

where A, B, and C are all formulas.

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:

(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

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`

if A then B end

is equivalent to the formula

if A then B else true end

For example, we might want our Fibonacci number predicate to print a warning message if we try to give it an index less than one, but to go on nevertheless:

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

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 A then B else if C then D else if E then F .... end end endIn this case, you can use the

if A then B elsif C then D elsif E then F endNote that only one

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

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 (

case term of

term_{1} => formula_{1};

term_{2} => formula_{2};

.................;

term_{n} => formula_{n};

end

term

term

.................;

term

end

The first term is called the subject term, and the others are called case terms; the formulas are called case conclusions. The subject term must be full-value, as is the case with variables in if condition formulas. One condition on the case terms must be met for the compiler to accept the case formula: they must, between them, cover all the possible forms that the subject term can take.

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

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 longpred 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

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

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

Top Modes Procedures, Subroutines and Functions