TY - JOUR
T1 - PLEASE
T2 - Executable specifications for incremental software development
AU - Terwilliger, Robert B.
AU - Campbell, Roy H.
PY - 1989/9
Y1 - 1989/9
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=0024736076&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0024736076&partnerID=8YFLogxK
U2 - 10.1016/0164-1212(89)90022-8
DO - 10.1016/0164-1212(89)90022-8
M3 - Article
AN - SCOPUS:0024736076
SN - 0164-1212
VL - 10
SP - 97
EP - 112
JO - The Journal of Systems and Software
JF - The Journal of Systems and Software
IS - 2
ER -