PLEASE: Executable specifications for incremental software development

Robert B. Terwilliger, Roy H. Campbell

Research output: Contribution to journalArticlepeer-review


PLEASE is an executable specification language that supports software development by incremental refinement. PLEASE is part of the ENCOMPASS environment that provides automated support for all aspects of the development process. In ENCOMPASS, software components are first specified using a combination of conventional programming languages and predicate logic. These abstract components are then incrementally redefined into components in an implementation language. Each refinement is verified before another is applied; therefore, the final components produced by the development satisfy the original specifications. PLEASE allows a procedure or function to be specified using pre- and post-conditions, a data type to have an invariant, and an implementation to be completely annotated. PLEASE specifications may be used in proofs of correctness; they may also be transformed into prototypes which use Prolog to "execute" pre- and post-conditions. We believe the early production of executable prototypes will enhance the development process.

Original languageEnglish (US)
Pages (from-to)97-112
Number of pages16
JournalThe Journal of Systems and Software
Issue number2
StatePublished - Sep 1989

ASJC Scopus subject areas

  • Software
  • Information Systems
  • Hardware and Architecture


Dive into the research topics of 'PLEASE: Executable specifications for incremental software development'. Together they form a unique fingerprint.

Cite this