PLEASE is an executable specification language that supports program development by incremental refinement. The authors present the PLEASE specification for a small library database. PLEASE is part of the ENCOMPASS environment, that provides automated support for all aspects of the software development process. Software components are first specified using a combination of conventional programming languages and predicate logic. These abstract components are then incrementally refined 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 with pre- and postconditions written using Horn clauses. PLEASE specifications may be used in proofs of correctness. They may also be transformed into prototypes that use Prolog to execute pre- and postconditions.
|Original language||English (US)|
|Title of host publication||Unknown Host Publication Title|
|Number of pages||8|
|State||Published - Jan 1 1987|
ASJC Scopus subject areas