PLEASE(ID:6976/)for Predicate Logic based ExecutAble SpEcifications Ada with path expressions (horn clauses) from Prolog, outputs (Quintus) Prolog code. Constraints nad definition mechanism inspired by the VDM Part of the SAGA project, used with the ENCOMPASS environment, evolved from earlier Path Pascal Related languages
References: DOI in [ACM SIGACT-SIGPLAN] Proceedings of the 11th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages POPL 84 1984 , Salt Lake City, Utah, United States view details in [ACM SIGACT-SIGPLAN] Proceedings of the 11th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages POPL 84 1984 , Salt Lake City, Utah, United States view details In ENCOMPASS, a development passes through the phases planning, requirements definition, validation, refinement, and system integration. This structure is the traditional lifecycle model extended to support, the Vienna Development Method (VDM) and the use of an executable specification language, in VDM, a program is first specified using elements from both conventional programming languages and mathematics. This specification is then incrementally transformed into a program in an implementation language. Each transformation is verified before another is applied, therefore the final program produced satisfies the original specification. In ENCOMPASS, VDM specifications may be written in the executable specification language PLEASE. Prototypes produced from PLEASE specifications may be used in the validation phase to enhance customer/developer communication. The use of PLEASE specifications also allows the verification of system components using either testing or proof techniques. In ENCOMPASS, the objects in a software system are modeled as entities which have relationships between them. Entities are grouped into modules and modules are grouped into projects. An entity, module or project may have different versions. A view of a project may be used to hide or expose entities, provide a different modularization, or emphasize different relationships. The entities considered by ENCOMPASS include: module specifications, bodies, object code, and load modules; test eases, drivers and harnesses; proofs of correctness; and all forms of documentation. ENCOMPASS supports multiple programmers and projects using a hierarchical library system containing a workspace for each programmer, a project library for each project, and a global library common to all projects. A workspace contains objects which are private to a single programmer, and possibly references to objects which are actually in libraries. The project leader controls access to the project library, which contains objects that must be available to all the personnel on a particular project. The global library contains objects available for reuse on all projects and is read-only to all but the librarian. The librarian reviews completed projects, decides which objects are suitable for reuse, and caters these objects into the library indexed by key words. A programmer may search the library for objects which are indexed on a number of key words and then create a copy of, or reference to, these objects in his workspace. A prototype implementation of ENCOMPASS is being constructed on a VAX running 4.2BSD UNIX using an existing revision control system. The system will incorporate may tools developed by the SAGA project, including a language-oriented editor and a proof management system. The initial prototype of ENCOMPASS will be used by the SAGA group in the development of future versions of ENCOMPASS and other software tools. in [ACM SIGACT-SIGPLAN] Proceedings of the 11th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages POPL 84 1984 , Salt Lake City, Utah, United States view details DOI Extract: Introduction Introduction It is widely acknowledged that producing correct software is both difficult and expensive. To help remedy this situation, methods of specifying and verifying software have been developed. The SAGA (Software Automation, Generation and Administration) project is investigating both the for real and practical aspects of providing automated support for the full range of software engineering activities. PLEASE is a language being developed by the SAGA group to support the specification, prototyping, and rigorous development of software components. In this paper we describe the development methodology for which PLEASE was created, give an example of development using the language, and describe the methods used to prototype PLEASE specifications. A life-cycle model describes the sequence of distinct stages through which a software product passes during its lifetime. There is no single, universally accepted model of the software life-cycle. The stages of the life-cycle generate software components, such as code written in programming languages, test data or results, and many types of documentation. In many models, a specification of the system to be built is created early in the lit%-cycle; as components are produced they are verified for correctness with respect to this specification. The specification is validated when it is shown to satisfy the customers requirements. Producing a valid specification is a difficult task. The users of the system may not really know what they want, and they may be unable to communicate their desires to the development team. If the specification is in a formal notation it may be an ineffective medium for communication with the customers, but natural language specifications are notoriously ambiguous and incomplete. Prototyping and the use of executable specification languages have been suggested as partial solutions to these problems. Providing the customers with prototypes for experimentation and evaluation early in the development process may increase customer/developer communication and enhance the validation and design processes. To help manage the complexity of software design and development, methodologies which combine standard representations, intellectual disciplines, and well defined techniques have been proposed. For example, it has been suggested that top-down development can help control the complexity of ~ program construction. By using stepwise refinement to create a concrete implementation from an abstract specification we divide the decisions necessary into smaller, more comprehensible groups. Methods to support the top-down development of programs have been devised and put into use. It has also been proposed that software development may be viewed as a sequence of transformations between specifications written at different linguistic levels; systems to support similar development methodologies have been constructed. Extract: VDM and PLEASE The Vienna Development Method supports the top-down development of programs specified in a notation suitable for mathematical verification. In this method, programs are first written in a language combining elements from conventional programming languages and mathematics. A procedure or function may be specified using pre and post-conditions written in predicate logic; similarly, an invariant ,nay be specified for a data type. Then these abstract programs are incrementally refined into programs in an implementation language. The refinements are performed one at a time, and each is verified before another is applied; therefore, the final program produced by the development satisfies the original specification. Extract: Path Pascal and PLEASE Path Pascal is an extension to standard Pascal allowing concurrent programming and encapsulated data types. In Path Pascal, a process is a program structure which has an independent thread of execution; independently executing processes communicate through shared data structures. Encapsulated data types called objects are manipulated only by the predefined routines associated with the type. Path expressions specify synchronization constraints that apply to the execution of the processes, functions and procedures within objects. Extract: about PLEASE PLEASE is an extension of Path Pascal, which supports a methodology similar to the Vienna Development Method. In PLEASE, a procedure or function may be specified with pre- and post-conditions written in predicate logic, and similarly an object may be specified using an invariant. For ease of expression, several data types have been added to the language. PLEASE specifications may be used in proofs of correctness; they also may be transformed into prototypes which use Prolog to "execute" pre- and post conditions, and may interact with other modules written in conventional languages. We believe that the early production of executable prototypes for experimentation and evaluation will enhance the software development process. Extract: Plan In section two of this paper, we describe the development methodology PLEASE was designed to support, and in section three, we give an example of program development using PLEASE. First we discuss an example program specification and describe how an executable prototype could be created for it. Then we show a refinement of this specification and discuss the process of verifying that the refined specification satisfies the original. In section four, we give an example of data type specification in PLEASE, and in section five, we discuss the implementation of the system, in section six, we describe tile work we have planned for the future and in section seven, we summarize and draw some conclusions from our experience. in [ACM SIGACT-SIGPLAN] Proceedings of the 11th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages POPL 84 1984 , Salt Lake City, Utah, United States view details in [ACM SIGACT-SIGPLAN] Proceedings of the 11th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages POPL 84 1984 , Salt Lake City, Utah, United States view details in [ACM SIGACT-SIGPLAN] Proceedings of the 11th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages POPL 84 1984 , Salt Lake City, Utah, United States view details in [ACM SIGACT-SIGPLAN] Proceedings of the 11th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages POPL 84 1984 , Salt Lake City, Utah, United States view details in [ACM SIGACT-SIGPLAN] Proceedings of the 11th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages POPL 84 1984 , Salt Lake City, Utah, United States view details in SIGPLAN Notices 23(04) April 1988 view details in SIGPLAN Notices 23(04) April 1988 view details in SIGPLAN Notices 23(04) April 1988 view details 1. Introduction Software development with abstract data types is usually done by first specifying the types and next implementing them. Specifications may be formal (equational) or not, and in the first case they may be executable or not. In this framework, two main questions arise: how can we prove the correctness of an implementation with respect to its specification? and, is there any help to transform a specification in an implementation? Roughly speaking, we may distinguish between formal verification and testing for the first question. Formal verification is better than testing because it assures the correctness of programs; however, it may be difficult to carry out, even with the help of appropriate tools, and this is why testing is still in use. Concerning the second question, specifications and implementations may be kept separated in different stages, interfering with software evolution, or else they may be joined together with a multiparadigm (wide-spectrum) language (which may be really a single language or else the combination of two or more existing languages into a single framework); in the second case, evolution may be performed with the help of some transformation rules or not. In this paper, we propose a multiparadigrn language combining equational specifications and imperative programs into a single framework. Even more, we require specifications to be operational (executable), and thus we adopt a testing approach to implementation correctness. To provide programmers with a great flexibility, we build an execution procedure that permits execution of software that combines specifications and imperative programs in an arbitrary manner; as a result, we may adopt a prototyping software development model in which a program is obtained by applying a sequence of refinement steps starting from a formal, possibly incomplete specification of the problem, being able to prototype the product at every stage of development by combining a term-rewriting system and an interpreter. We remark that our prototyping strategy does not prevent the use of a transformational approach. On the other hand, this kind of testing may be sometimes employed as a complement of formal verification to show the execution behaviour of a piece of software (for instance, to study interfaces with the user). Also, we remark the flexibility of the strategy, that does not oblige neither the specification of a data type before its implementation (we may think in those procedural aspects which specification really looks as an implementation) nor any fixed "implementation rate" (implementations may be built and tested at once, or function by function); in any case, execution is always possible. The rest of the paper is organised as follows. In section 2, we present the multiparadigm notation used in the paper. In section 3, it is shown how may we customise the execution environment. In section 4, the execution procedure is presented from some demonstrably correct transformation rules, and an example is shown in section 5. Finally, section 6 remarks some undesirable issues of the work, and section 7 gives the conclusions and future work. Extract: A multiparadigm language A multiparadigm language The ideas we present in this paper are intended not to be tied to any concrete programming language: they may be applied to a specification language as OBJ [FGMJ85] or ACT ONE [EM85], linked with any imperative programming language as Ada, Modula or O.-O. ones. Also, they may be applied to any equational enrichment of an imperative programming language (Ada with equations, as Anna [LH85]), or (with a few modifications) even to logic programming combined with imperative programming (as in [DDL88, Rad90]). To be as general as possible, we use in the paper an ad hoc notation based on the concept of abstract data type as design unit. It allows: on the one hand, formal, possibly incomplete specification of types as a previous step to their implementation; on the other hand, gradual implementation of those types supported by a programming environment, which is able to incrementally execute programs, even if they do combine specified types with implemented ones. Data type encapsulation mechanisms are called universes; they may define new types (probably parameterised), or enrichments of types by adding new operations on some existing ones; depending on their contents, we talk about specification universes or implementation universes. Specification universes present some constructs to define type signatures (that is, types' names -called sorts- and operations) and properties. Properties are stated in equational style; equations may be conditional, the conditions in turn being equations. The logic to express equations allows to associate initial semantics to specifications [GTW78] and thus it is possible to use a term-rewriting system to manipulate terms during execution of programs. Implementation universes' notation presents Ada-like programming language constructs. Each implementation universe must be referred to a specification one (which presents at least the signature of the type) and it may include data structures and/or functions with no side-effects. In many contexts, prototyping can take place only if there exists an abstraction function [Hoa72] to find out which value of a type is represented by a particular state of the implementation. Thus, implementation universes should provide this function in order to be able to prototype the execution in any intermediate state; in spite of being defined in implementation universes, the abstraction function may be stated either in equational or imperative style. In both kinds of universes some structuring mechanisms can be employed. The basic one is the use of specifications, which makes all the symbols exported by a specification universe available to its users. There is also a parameterisation facility to define generic universes, coupled with a parameter passing mechanism (instantiation); formal parameters are defined in the so-called characterisation universes. Last, there are some constructs to control the scope of symbols in specifications: symbols may be renamed, hidden or introduced as private from the very beginning. As an example, we give the highlights of the specification of a generic type for directed, unlabelled graphs and its implementation with adjacency matrix. In the specification, the parameters are the node's type el em and an equality operator eq (to specify membership), both of them defined in the characterisation universe ELEM_= (the first one as a sort and the second one as an operation which properties are stated), empty and add are the so-called generating operations, which "generate" all the values of the type and that serve as the basis for the specification of the other operations in the initial semantics framework. Note the use of specifications of booleans, the definition of auxiliary functions, the instantiation and renaming of a generic type for lists in order to define the signature, the specification of erroneous situations and the use of conditional equations. The abstraction function is given in imperative style; when this is the case, a variable of a generic type term is used to hold the result. Also, a representation invariant is provided, which may be used during execution. In the general case, there may be many levels of implementations; for instance, graphs may be also implemented by (adjacency) lists, which may implemented by arrays in turn. Anyway, the bottom level consists of predefined types like arrays and integers. Last, let's make clear some language concepts from the execution point of view. First of all, there is no main program in applications; instead, we may pick up any function to be the subject of execution at any time. As a result, we may assimilate the notion of execution to the idea of evaluating a term, that is, the application of a function over its parameters. Throughout the paper, a term is called an expression when it is used in a context that requires its evaluation; note that an expression may contain many proper sub expressions. Inside expressions, objects do appeal- which will be evaluated in the appropriate moments (we denote by the word object any of the following entities: variables, parameters, constants -predefined or user-defined- and function results). As a key point during execution, objects' value may be either a data structure or a term; in the first case, we talk about implemented objects, while we call specified objects the second ones. Note that objects may be intertwined due to the existence of many levels of implementation; that is, an object of type graph may be implemented with an array, being their components of type list which may be specified (if there not exist an implementation for it), and elements inside lists (for instance, integers) may be implemented in turn. In this case we talk about hybrid objects. The figure below illustrates this situation. Extract: Conclusions and future work Conclusions and future work A framework for software development by means of prototyping has been presented. We use an abstract data type oriented language that combines equations and imperative programs, and thus software refinement consists of gradually transforming the specified types into implemented ones, being able to prototype the application at any stage of development, provided that specifications are operational and that an abstraction function and a representation invariant do exist for every implementation. Being evaluation of expressions the main issue of execution, we have identified many rules to transform an expression assuring that its value is preserved; the crucial fact is how specified and implemented functions and values coexist. Then, we have formulated an execution procedure which gives preference to testing over efficiency and which involves a term rewriting system to evaluate specified functions and an interpreter for imperative ones. Other projects do exist that support execution of equations mixed with imperative programs. The closest to ours is the execution system of Asspegique [CK90], which combines PLUSS specifications with Ada implementations. There is a basic difference, however: mixed execution relies on the compilation of equations into Ada and in the generation of packages for the involved modules. We think that, in the testing framework, compilation prevents the easy interaction between the user and the execution system, as well as quick and interactive modifications of the rewrite rules and customisation of the environment. This compilation scheme has been adopted by many other teams [DDL88, Rad90]. About the future work, we want to allow mixed execution even if more than one implementation for the same type is used in different contexts of the same program. This issue has been addressed in [Fra94] and the integration into the current work seems to be natural: no new constructions are required over the language (the abstraction function is enough) and initial semantics still provides a valid formal framework. On the other hand, efficiency of computations should be improved. Mainly, we are studying the interest of sharing of subterms and the advantages of maintaining a twofold value in objects (the result of an abstraction and the value before abstraction). We are also considering the possibility of a lazy implementation of the final evaluation, which would be possible due to the sharing of subterms. in Procs. 7th International Symposium on Programming Languages: Implementations, Logics and Programs (PLILP), Utrecht (The Netherlands), September 1995, LNCS 982, view details |