Please: Predicate logic based executable specifications1

Robert B. Terwilliger, Roy H. Campbell

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

PLEASE is an executable specification language which supports program development by incremental refinement. Software components are first specified using a combination of conventional programming languages and mathematics. These abstract components are then incrementally refined into components ill an implementation language. Each refinement is verified before another is applied; therefore, the final components produced by the development satisfy the original specilieations. PLEASE allows a procedure or function to be specified using pre- And post-conditions written in predicate logic and all abstract data type to have a type invariant. PLEASE specifications may be used in proofs of correctness, and may also be transformed into prototypes which use Prolog to "execute" pre- And post-conditions. The early production of executable prototypes for experimentation and evaluation may enhance the development process.

Original languageEnglish (US)
Title of host publicationProceedings of the 1986 ACM 14th Annual Conference on Computer Science, CSC 1986
PublisherAssociation for Computing Machinery, Inc
Pages349-358
Number of pages10
ISBN (Electronic)0897911776, 9780897911771
DOIs
StatePublished - Feb 1 1986
Event1986 ACM 14th Annual Conference on Computer Science, CSC 1986 - Cincinnati, United States
Duration: Feb 4 1986Feb 6 1986

Publication series

NameProceedings of the 1986 ACM 14th Annual Conference on Computer Science, CSC 1986

Other

Other1986 ACM 14th Annual Conference on Computer Science, CSC 1986
Country/TerritoryUnited States
CityCincinnati
Period2/4/862/6/86

ASJC Scopus subject areas

  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Please: Predicate logic based executable specifications1'. Together they form a unique fingerprint.

Cite this