% Save file as: PROGRAM-DEMO.TEX       Source: FILESERV@SHSU.BITNET  
\documentstyle[11pt,a4,program]{article}
\setlength{\parskip}{2ex}

% Set up the commands for all those extremely_long_keywords_in_pascal:
\newcommand{\comm}{|l_hyd_iso_test_command|}
\newcommand{\HY}[1]{|hyd_cond.#1|}
\newcommand{\RI}[1]{|rt_in.#1|}
\newcommand{\RO}[1]{|rt_out.#1|}
\newcommand{\mode}{|l_hyd_iso_test_mode|}
\newcommand{\dem}{|l_hyd_isovlv_dem|}
\newcommand{\state}{|l_hyd_iso_vlv_state_data|}
\newcommand{\press}{|l_hyd_util_press_loss|}
\newcommand{\fail}{|l_hyd_iso_fail|}
\newcommand{\res}{|l_hyd_iso_res_low|}
\newcommand{\speed}{|l_gb_speed|}
\newcommand{\gb}{|c_gb_59|}
\newcommand{\valid}{|l_gb_speed_valid|}

\begin{document}
\title{A demonstration of the {\bf program} environment}
\author{Martin Ward\\
Centre for Software Maintenance\\
University of Durham}
\maketitle

\tableofcontents

\section{Example with |first_set| and $|first_set|$}

Here is a small program: \( |first_set|:= \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.

You can use |variable_names| in text or math mode: $|variable_name|»2 = 2$.

Note that \verb:\(: and \verb:\): are redefined to typeset a program in
a minipage (useful in running text, or to keep a short program all on
one page). There is some notation for sequences: \( \seq{x_1,x_2,\dots,x_n} \)
and for universal and existential quantifiers: $ \Forall x. \Exists 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 \S1, \S2, \S{23}) or a
sequence of ``prime'' characters: \S', \S''''' etc.

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

\noindent
% programbox keeps the program on one page - like parbox
\begin{programbox}
\IF \T1
    \THEN \IF \T2
	      \THEN \IF \T3
			\THEN \S4
			\ELSE \S3
		    \FI
	      \ELSE \S2
	  \FI
    \ELSE \S1
\FI;

\IF \T1 \THEN \IF \T2 \THEN \IF \T3 \THEN \S4
				    \ELSE \S3 \FI
		      \ELSE \S2 \FI
	\ELSE \S1 \FI;
\end{programbox}

\noindent
Here's a larger example,
a transcription from a real-time PASCAL program:
\begin{program}
\IF \B1 \AR |t1|:=0; |t2a|:=0; |t2b|:=0; |t3|:=0; \S1; \S5
\BAR \B2 \AR |t2a|:=0; |t2b|:=0; |t3|:=0; \S2; \S7;
	     \IF \T1 \THEN \S3
		     \ELSE |t1|:= |t1| + 1 \FI
\BAR \B{} \AR |t1|:=0;
	     \IF \A1 \AR |t2b|:=0; |t3|:=0;
		  \IF \R{} \THEN \IF \NOT\T{2a} \THEN |t2a|:= |t2a| + 1 \FI;
					\S7; \S4; \S6;
			  \ELSF \NOT\T{2a} \THEN |t2a|:= |t2a| + 1; \S5
					   \ELSE \S6 \FI;
	     \BAR \A2 \AR |t2a|:=0; |t3|:=0;
		  \IF \R{} \THEN \IF \NOT\T{2b} \THEN |t2b|:= |t2b| + 1 \FI;
					\S7; \S4; \S6
			  \ELSF \NOT\T{2b} \THEN |t2b|:= |t2b| + 1; \S5
					   \ELSE \S6 \FI;
	     \BAR \A3 \AR |t2a|:=0; |t2b|:=0
			  \IF \R{} \THEN \IF\NOT\T3 \THEN |t3|:= |t3| + 1
						   \ELSE \S3 \FI;
					\S7; \S6;
				  \ELSE |t3|:=0; \S8 \FI \FI \FI
\end{program}


Just to show that {\tt \origbar} still works normally (to indicate the
placing of vertical lines) in the preamble of a tabular
(or array) environment:

\begin{tabular}{|r|l|} \hline
\bf Statement & \bf Conditions  \\
\hline
\S1     & \B1 \\
\S2     & \B2 \\
\S3     & $(\B2 \AND \T1 )\OR (\B3 \AND \A3 \AND \R{} \AND \T3 )$ \\
\S4     & $(\B3 \AND \R{} \AND \A1 )\OR (\B3 \AND \R{} \AND \A2 )$ \\
\S5     & $\B1 \OR (\B3 \AND \A1 \AND \NOT\R{} \AND \NOT\T{2a} )\OR
		   (\B3 \AND \A2 \AND \NOT\R{} \AND \NOT\T{2b} )$ \\
\S6     & $(\B3 \AND \R{} \AND \A1 )\OR (\B3 \AND \R{} \AND \A2 )\OR
				      (\B3 \AND \R{} \AND \A3 )$ \\
\S7     & $\B2 \OR (\B3 \AND \R{} \AND \A1 )\OR
		   (\B3 \AND \R{} \AND \A2 )\OR (\B3 \AND \R{} \AND \A3 )$ \\
\S8     & $(\B3 \AND \A3 \AND \NOT\R{} )$ \\
|t1|:=0 & $\B1 \OR \B3 $ \\
|t2a|:=0& $\B1 \OR \B2 \OR (\B3 \AND \A2 )\OR (\B3 \AND \A3 )$ \\
|t2b|:=0& $\B1 \OR \B2 \OR (\B3 \AND \A1 )\OR (\B3 \AND \A3 )$ \\
|t3|:=0 & $\B1 \OR \B2 \OR (\B3 \AND \A1 )\OR (\B3 \AND \A2 )\OR
	       (\B3 \AND \A3 \AND \NOT\R{} )$ \\
|t1|:= $ |t1| + 1 $     & $(\B2 \AND \NOT\T1 ) $\\
|t2a|:= $ |t2a| + 1 $   & $(\B3 \AND \A1 \AND \NOT\T{2a} )$ \\
|t2b|:= $ |t2b| + 1 $   & $(\B3 \AND \A2 \AND \NOT\T{2b} )$ \\
|t3|:= $ |t3| + 1 $     & $(\B3 \AND \A3 \AND \R{} \AND \NOT\T3 )$ \\
\hline
\end{tabular}

\noindent The notation for procedures and functions:

\noindent
\begin{programbox}
\mbox{A fast exponentiation function:} \\ % Use \mbox for comments
\BEGIN %
  \FOR i:=1 \TO 10 \STEP 1 \DO
     |print|(|expt|(2,i)); \\ |newline|() \OD
\WHERE
\FUNCT |expt|(x,n) \BODY
	  \EXP z:=1;
	       \WHILE n \ne 0 \DO
		  \WHILE |even|(n) \DO
		     n:=n/2; x:=x*x \OD;
		  n:=n-1; z:=z*x \OD;
	       z \ENDEXP \ENDFUNCT
\END
\end{programbox}

\noindent
\begin{programbox}
\mbox{A fast exponentiation procedure:}
\BEGIN %
  \FOR i:=1 \TO 10 \STEP 1 \DO
     |expt|(2,i); \\ |newline|() \OD %
		\rcomment{A comment flush to the right margin}
\WHERE
\PROC |expt|(x,n) \BODY
	  z:=1;
	  \DO \IF n=0 \THEN \EXIT \FI;
	     \DO \IF |odd|(n) \THEN \EXIT \FI;
		n:=n/2; x:=x*x \OD;
	     n:=n-1; z:=z*x \OD;
	  |print|(z) \ENDPROC
\END
\end{programbox}

\noindent An action system: %
\begin{programbox}
  \A1 \EQ \S1; \\ \S2; \\ \A2 \QE
  \A2 \EQ \IF \B{} \THEN \S1
		      \ELSE \S2; \A3 \FI \QE
  \A3 \EQ \IF \T{} \THEN \A1 \ELSE \Z{} \FI \QE
  |tidy_up| %
\end{programbox} Note the use of the \Z{} action.

\noindent Dijkstra conditionals and loops:
\begin{program}
\IF x = 1 \AR y:=y+1
\BAR x = 2 \AR y:=y»2
\BAR x = 3 \AR y:=\sum_1»n y_i \FI

\DO 2 \origbar x \AND x>0 \AR x:= x/2
\BAR \NOT 2 \origbar x    \AR x:= x+3 \OD
\end{program}

\noindent Loops with multiple \keyword{exit}s:
\begin{program}
\DO \DO \IF \B1 \THEN \EXIT \FI;
	\S1;
	\IF \B2 \THEN \EXIT(2) \FI \OD;
    \IF \B1 \THEN \EXIT \FI \OD
\end{program}

I hope you get the idea!

\end{document}
