A demonstration of the program environment

Martin Ward Centre for Software Maintenance University of Durham

February 26, 1997

Contents

1 Example with first set and first set. 1

2 Procedures and Functions 3

3 A Reverse Engineering Example 4

1 Example with first set and first set.

The program style defines two environments, program and programbox for typesetting programs and algorithms. Within the program environment:

1. Newlines are significant;

2. Each line is in math mode, so for example spaces in the input file are not significant;

3. The command \\ within a line causes an extra linebreak in the output;

4. The indentation of each line is calculated automatically;

5. To cause extra indentation, use the commands \tab to set a new tab, and \untab to remove it (see the examples below);

6. Vertical bars are used to delimit long variable names with underscores (and other unusual characters).

   testing | in verbatim
testing | in verbatim

Here is a small program: first set := { x | x^{2} + y_{1} > 0 } It shows how to typeset mathematics as part of a program. Since each line is typeset in maths mode, all spacing is done automatically. The set brackets expand automatically, for example in this program (which also demonstrates the \tab and \untab commands):

t := \{ x | \frac{x}{y} = z \};

t := t \ u; z := a + b + c + d

+ e + f + g

+ h + i + j;

\underline{if} x = 0 \underline{then} y := 0 \underline{fi}

You can use variable names in text or math mode: variable name^{2} = 2. Names can have odd characters:!@#$%ˆ &*:; like this!.

Note that \( and \) are redefined to typeset a program in a minipage. (This is useful in running text, or to keep a short program all on one page). There is some notation for sequences: ⟨x_{1}, x_{2}, …, x_{n}⟩ and for universal and existential quantifiers: ∀x. ∃y. y > x (yes, I use these in my programs!)

I often use bold letters to represent program fragments, formulas etc. so I have set up commands S, R etc. for the most common ones. The commands have one argument (a subscript, eg S_{1}, S_{2}, S_{23}) or a sequence of “prime” characters: S′, S′′′′′ etc. If you want both a subscript and one or more primes, then you must use maths mode, eg S′_{2} Consider the difference between typing ``\S2'' which gives “S_{2}” and ``$\S2''$'' which gives “S′′_{2}”. Outside maths mode, \S assumes any primes after a subscript are either closing quotes or apostrophes.

Here are two program examples with different indentation styles. Note that all indentation is calculated automatically in either style:

\underline{if} T_{1}
\underline{then} \underline{if} T_{2}
\underline{then} \underline{if} T_{3}
\underline{then} S_{4}
\underline{else} S_{3}

\underline{fi}

\underline{else} S_{2}

\underline{fi}

\underline{else} S_{1}

\underline{fi};

\underline{if} T_{1} \underline{then} \underline{if} T_{2} \underline{then} \underline{if} T_{3} \underline{then} S_{4}
\underline{else} S_{3} \underline{fi}
\underline{else} S_{2} \underline{fi}
\underline{else} S_{1} \underline{fi};

Note that \underline{then} and \underline{else} should be at the start of a line (as in the examples above), not at the end. This is so that you can line them up in short \underline{if} statements, for example:

\underline{if} x = 1 \underline{then} a long procedure name(arg1, arg2, …)

\underline{else} another long procedure name(arg1, arg2, …) \underline{fi}

If the test is long, then you probably want an extra linebreak:

\underline{if} a long boolean function name?(arg1, arg2, …)

\underline{then} a long procedure name(arg1, arg2, …)

\underline{else} another long procedure name(arg1, arg2, …) \underline{fi}

Compare this with the following (which has linebreaks in the “wrong” places):

\underline{if} a long boolean function name?(arg1, arg2, …) \underline{then}

a long procedure name(arg1, arg2, …) \underline{else}

another long procedure name(arg1, arg2, …) \underline{fi}

Just to show that | still works normally to indicate the placing of vertical lines) in the preamble of a tabular (or array) environment:

Statement Conditions
S_{1} B_{1}
S_{2} B_{2}

2 Procedures and Functions

Turning on line numbering here. Also using the algoritm enviroment to number the algorithms within the sections.

Algorithm 2.1

1 A fast exponentiation function:
2 \underline{begin} \underline{for} i := 1 \underline{to} 10 \underline{step} 1 \underline{do}
3  print(expt(2, i));
4  newline() \underline{od}
5 \underline{where}
6 \underline{funct} expt(x, n) ≡
7 z := 1;
8  \underline{while} n ≠ 0 \underline{do}
9  \underline{while} even(n) \underline{do}
10  n := n/2; x := x ∗ x \underline{od};
11  n := n − 1; z := z ∗ x \underline{od};
12 z .
13 \underline{end}

First line is line 1, last is line 13. Line 10 is what makes this function fast!

Algorithm 2.2

1 A fast exponentiation procedure:
2 \underline{begin} \underline{for} i := 1 \underline{to} 10 \underline{step} 1 \underline{do}
3  expt(2, i);
4  newline() \underline{od} This text will be set flush to the right margin
5 \underline{where}
6 \underline{proc} expt(x, n) ≡
7 z := 1;
8  \underline{do} \underline{if} n = 0 \underline{then} \underline{exit} \underline{fi};
9  \underline{do} \underline{if} odd(n) \underline{then} \underline{exit} \underline{fi};
10  \underline{comment}: This is a comment statement;
11  n := n/2; x := x ∗ x \underline{od};
12  {n > 0};
13  n := n − 1; z := z ∗ x \underline{od};
14 print(z).
15 \underline{end}

An action system equivalent to a \underline{while} loop:

1 \underline{actions} A :
2 A ≡ \underline{if} B \underline{then} S; \underline{call} A
3  \underline{else} \underline{call} Z \underline{fi}.
4 \underline{endactions}

≈

1 \underline{while} B \underline{do} S \underline{od}

Note the use of \( and \) to enclose the two program boxes. Turning off line numbers here.

Dijkstra conditionals and loops:

\underline{if} x = 1 → y := y + 1 ⊓ ⊔ x = 2 → y := y^{2} …

⊓ ⊔ x = n → y := ∑_{i=1}^{n} y_{i} \underline{fi}

\underline{do} 2|x ∧ x > 0 → x := x/2 ⊓ ⊔ ¬2|x → x := |x + 3| \underline{od}

Loops with multiple \underline{exit}s:

\underline{do} \underline{do} \underline{if} B_{1} \underline{then} \underline{exit} \underline{fi}; S_{1};

\underline{if} B_{2} \underline{then} \underline{exit}(2) \underline{fi} \underline{od};
\underline{if} B_{1} \underline{then} \underline{exit} \underline{fi} \underline{od}

I hope you get the idea!

3 A Reverse Engineering Example

Here’s the original program:

Algorithm 3.1

\underline{var} ⟨m := 0, p := 0, last := “ ”⟩; \underline{actions} prog : prog ≡

⟨line := “ ”, m := 0, i := 1⟩;

\underline{call} inhere.

l ≡ i := i + 1; \underline{if} (i = (n + 1)) \underline{then} \underline{call} alldone \underline{fi}; m := 1; \underline{if} item[i] ≠ last

\underline{then} write(line); line := “ ”; m := 0;

\underline{call} inhere \underline{fi};

\underline{call} more.

inhere ≡ p := number[i]; line := item[i]; line := line ++ “ ” ++ p;

\underline{call} more.

more ≡

\underline{if} (m = 1) \underline{then} p := number[i];

line := line ++ “, ” ++ p \underline{fi};

last := item[i]; \underline{call} l.

alldone ≡ write(line); \underline{call} Z. \underline{endactions} \underline{end}

And here’s the transformed and corrected version:

Algorithm 3.2

⟨line := “ ”, i := 1⟩; \underline{while} i ≠ n + 1 \underline{do}

line := item[i] ++ “ ” ++ number[i];

i := i + 1;

\underline{while} i ≠ n + 1 ∧ item[i] = item[i − 1] \underline{do} line := line ++ “, ” ++ number[i]); i := i + 1 \underline{od};

write(line) \underline{od}

These are the same programs in a sans-serif style, using the command

\sfvariables:

var ⟨m := 0, p := 0, last := “ ”⟩; actions prog : prog ≡

⟨line := “ ”, m := 0, i := 1⟩;

call inhere.

l ≡ i := i + 1; if (i = (n + 1)) then call alldone fi; m := 1; if item[i] ≠ last

then write(line); line := “ ”; m := 0;

call inhere fi;

call more.

inhere ≡ p := number[i]; line := item[i]; line := line ++ “ ” ++ p;

call more.

more ≡

if (m = 1) then p := number[i];

line := line ++ “, ” ++ p fi;

last := item[i]; call l.

alldone ≡ write(line); call Z. endactions end

⟨line := “ ”, i := 1⟩; while i ≠ n + 1 do

line := item[i] ++ “ ” ++ number[i]; i := i + 1; while i ≠ n + 1 ∧ item[i] = item[i − 1] do

line := line ++ “, ” ++ number[i]); i := i + 1 od;

write(line) od