6.3 Conditional equations

Tutorial on SDL-88
Belina, Hogrefe (edits Reed)

A conditional equation is an equation that only holds if a certain condition holds. The general form of a conditional equation is:

condition ==> equation

The classical example of a conditional equation is the definition of division for real numbers:

FOR ALL x, z IN Real
(z/=0 == true ==> (x/z)*z == x);

The equation states that if z is not equal to zero, then division followed by multiplication with the same value has no effect. The conditional equation does not say anything about the case that z is equal to zero. This case can be treated in a different equation if necessary:

FOR ALL x, z IN Real
(z=0 == true==> (x/z)*z == Error!);

For reasons of readability, the two equations above can be combined into one equation using a so called conditional term. This always works if the two equations have complementary conditions:

FOR ALL. x, z IN Real
((x/z)*z == IF z/=0 THEN x ELSE Error! FI);