Program algebra for sequential code

AbstractThe jump instruction is considered essential for an adequate theoretical understanding of imperative sequential programming. Using basic instructions and tests as a basis we outline an algebra of programs, denoted PGA, which captures the crux of sequential programming. We single out a behavior extraction operator which assigns to each program a behavior. The meaning of the expressions of PGA is explained in terms of the extracted behavior. Using PGA a small hierarchy of program notations is developed. Projection semantics is proposed as a tool for the description of program semantics