Formal models of stepwise refinements of programs

Ali Mili, Jules Desharnais, Jean Raynomd Gagné

Research output: Contribution to journalArticlepeer-review

15 Scopus citations


Of the many ways to express program specifications, three of the most common are: as a pair of assertions, an input assertion and an output assertion; as a function mapping legal inputs to correct outputs; or as a relation containing the input/output pairs that are considered correct. The construction of programs consists of mapping a potentially complex specification into a program by recursively decomposing complex specifications into simpler ones. We show how this decomposition takes place in all three modes of specification and draw some conclusions on the nature of programming.

Original languageEnglish (US)
Pages (from-to)231-276
Number of pages46
JournalACM Computing Surveys (CSUR)
Issue number3
StatePublished - Sep 1 1986
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


  • Alternation rule
  • assertion-based specifications
  • assignment rule
  • function-based specifications
  • generalization rule
  • iteration rule
  • relationbased specifications
  • sequence rule


Dive into the research topics of 'Formal models of stepwise refinements of programs'. Together they form a unique fingerprint.

Cite this