Top Modes Procedures, Subroutines and Functions
French French German German ItalianItalian SpanishSpanish PortuguesePortuguese JapaneseJapanese KoreanKorean ChineseChinese

Control Structures


The if and case formulas of FormulaOne correspond to similar features of other programming languages. We can use these types of formulas to make common patterns of logic more readable, because they have a syntax and structure which is closer to what we are thinking when these patterns appear in our programs. Another reason to use if and case is that the FormulaOne compiler can compile them into very efficient object code.

The if Formula

We can rewrite Fib_prevl predicate by using an if formula. 
pred 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
    end
The general form of an if formula is:

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:

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 end
Normally 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
end
This 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.

Alternate Forms of if

There are two main alternate forms of the if formula. The formula

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 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
     end
In 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
    end
Note 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)
    end
Here'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

The case Formula

The case formula is similar to the if formula, in that it causes formulas to be evaluated based on the outcome of a test. Consider the following rewriting of the Sum1 predicate. 
pred Sum2(l :< list I, s :> I) iff
    {the sum of the members of '!' is 's'}
    case l of
       Nil         => s = 0;
      (head, tail) => Sum2(tail, tailsum) & s = head + tailsum
    end
The 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:

case term of
    term1 => formula1;
    term2 => formula2;
     .................;
    termn => formulan;
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.

This means, among other things, that 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, subrange types, and union types (which we'll discuss later) can be subject terms; all others, such as those of type I, cannot.

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'
    end
However, 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'
    end
The 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'
    end

Iteration

Most programming languages provide an explicit method of allowing iteration, or looping, where a segment of a code can be executed repeatedly. FormulaOne provides this facility by recursion.

Top Modes Procedures, Subroutines and Functions