Abstract
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 |
| Publisher | IEEE |
| Pages | 249-256 |
| Number of pages | 8 |
| ISBN (Print) | 0818607696 |
| State | Published - 1987 |
ASJC Scopus subject areas
- General Engineering