\documentclass{article}
\usepackage{listings}
\begin{document}
\lstset{language=GCL}
\lstset{escapeinside=`'}
\begin{lstlisting}[caption=Bounded Linear Search, frame=trbl]{}
|[ const N: int { N > 0 }; b: array[0..N) of bool;
   var x: int;
   |[ var y: int;
         x, y := 0, N
        ;do x != y
            -> if !b.x	-> x := x + 1
               [] b.x	-> y := x
               fi
         od
   ]|
   { `\ensuremath{x = (\textbf{max}~i: 0\leq i\leq N\land (\forall j: 0\leq j < i: \lnot b.j): i)}' }
]|
\end{lstlisting}
\begin{lstlisting}[caption=Binary Search, frame=trbl]{}
|[ const N, A: int { N >= 1 }; f: array[0..N] of int { f.0 <= A < f.N };
   var x: int;
   |[ var y: int;
         { 0 < N /\ f.0 <= A < f.N }
         x, y := 0, N
        ;do x+1 != y
            -> |[ var h: int;
                     h := (x+y) div 2
	            ;if f.h <= A	-> x := h
                     [] A < f.h		-> y := h
                     fi
	       ]|
         od
         { f.x <= A < f.(x+1) }
   ]|
   { f.x <= A < f.(x+1) }
]|
\end{lstlisting}
\end{document}
