Conjunction as composition
ACM Transactions on Software Engineering and MethodologyPublished 1 October 1993Open access
Pamela Zave, Michael Jackson
Citations206
SJR quartileQ1
SJR score1.28
SNIP2.11
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
The criteria for success are that a wide variety of specification languages should be accommodated, there should be no restrictions on where boundaries between languages can be placed, and intuitive expectations of the specifier should be met.
Abstract
Partial specifications written in many different specification languages can be composed if they are all given semantics in the same domain, or alternatively, all translated into a common style of predicate logic. The common semantic domain must be very general, the particular semantics assigned to each specification language must be conducive to composition, and there must be some means of communication that enables specifications to build on one another. The criteria for success are that a wide variety of specification languages should be accommodated, there should be no restrictions on where boundaries between languages can be placed, and intuitive expectations of the specifier should be met.
Keywords
Computer Science
Science of Computer ProgrammingStatecharts: a visual formalism for complex systems
6,691 Citations1987David Harel
It is intended to demonstrate here that statecharts counter many of the objections raised against conventional state diagrams, and thus appear to render specification by diagrams an attractive and plausible approach.
The temporal logic of programs
5,586 Citations1977Amir Pnueli
A unified approach to program verification is suggested, which applies to both sequential and parallel programs, and the main proof method is that of temporal reasoning in which the time dependence of events is the basic concept.
Prentice Hall International (UK) Ltd. eBooksSystematic software development using VDM
1,725 Citations1986Cli B. Jones
Logic of propositions reasoning about predicates functions and operations set notation composite objects and invariants map notation sequence notation data rectification more on data types operation decomposition.
ACM Computing SurveysOn understanding types, data abstraction, and polymorphism
1,675 Citations1985Luca Cardelli, Peter Wegner
A λ-calculus-based model for type systems that allows us to explore the interaction among the concepts of type, data abstraction, and polymorphism in a simple setting, unencumbered by complexities of production programming languages is developed.
IEEE Transactions on Software EngineeringSTATEMATE: a working environment for the development of complex reactive systems
1,117 Citations1990David Harel, H. Lachover +6 more
Principles of program design
904 Citations1975Michael Jackson
This book is about programming for data processing applications, and its purpose is to present a coherent method and procedure for designing systems, programs, and components that are transparently simple and self-evidently correct.
ComputerA specifier's introduction to formal methods
720 Citations1990J.M. Wing
Formal methods used in developing computer systems are defined, and their role is delineated, and certain pragmatic concerns about formal methods and their users, uses, and characteristics are discussed.
World Computer Congress on Algorithms, Software, ArchitectureA Formal Approach to Software Architectures
541 Citations1992Robert J. Allen, David Garlan
International Journal of Software Engineering and Knowledge EngineeringVIEWPOINTS: A FRAMEWORK FOR INTEGRATING MULTIPLE PERSPECTIVES IN SYSTEM DEVELOPMENT
527 Citations1992Anthony Finkelstein, Jennifer Kramer +3 more
This paper outlines a framework which supports the use of multiple perspectives in system development, and provides a means for developing and applying systems design methods.
IEEE Transactions on Software EngineeringThe transformation schema: An extension of the data flow diagram to represent control and timing
248 Citations1986Paul T. Ward
An extension of the data flow diagram called the transformation schema is described, which provides a notation and formation rules for building a comprehensive system model, and a set of execution rules to allow prediction of the behavior over time of a system modeled in this way.
Communications of the ACMA simple approach to specifying concurrent systems
237 Citations1989Leslie Lamport
The transition axiom method provides a conceptual and logical foundation for writing formal specifications; it is not a specification language and is not meant as a paradigm for how systems should be built.
Lecture notes in computer scienceFormalizing design spaces: Implicit invocation mechanisms
149 Citations1991David Garlan, David Notkin
It is argued that formal specification can help solve the problem of common properties of systems that are poorly understood and can help build new designs in a principled way, at reduced cost to designers and implementors.
Domain descriptions
109 Citations2002Michael Jackson, Pamela Zave
It is argued that current formal specification techniques are inadequate in this respect, and therefore cannot offer a satisfactory foundation for automated support of software development.
IEEE SoftwareWorking in the Garden Environment for Conceptual Programming
102 Citations1987Steven P. Reiss
This automated design system conforms to the programmer using a variety of techniques to create systems that meet the needs of the programmer.
IEEE SoftwareA compositional approach to multiparadigm programming
90 Citations1989Pamela Zave
The author points out that although different aspects of a system require different approaches, programmers are confined to their language's one paradigm, and multiparadigm programming makes it possible to match the paradigm to the problem.
IEEE Transactions on Software EngineeringRepresentation and presentation of requirements knowledge
88 Citations1992W. Lewis Johnson, Martin S. Feather +1 more
The approach to representation and presentation of knowledge used in ARIES, an environment to experiment with support for analysts in modeling target domains and in entering and formalizing system requirements, is described.
IEEE Transactions on Software EngineeringA case-study in timed refinement: a mine pump
74 Citations1992Brendan Mahony, Ian J. Hayes
A specification and top-level refinement of a simple mine pump control system, as well as a proof of correctness of the refinement, are presented as an example of the application of a formal method for the development of time-based systems.
Communications of the ACMSpecification-level interoperability
71 Citations1991Jack C. Wileden, Alexander L. Wolf +2 more
The authors discuss the representation-level and specification-level approaches to interoperability, describe the current prototype realization of the specification- level approach and their experience with its use, and outline their plans for extending both the approach and its realization.
International Conference on Software Engineering“…And nothing else changes”: the frame problem in procedure specifications
55 Citations1993Alex Borgida, John Mylopoulos +1 more
Science of Computer ProgrammingImplementing specification freedoms
53 Citations1982Philip London, Martin S. Feather
Mapping issues are discussed in the context of the development methodology, in which implementations are derived via the application of correctness-preserving transformations applied to a specification language whose high-level expressive capabilities are modeled after natural language.
IEEE Transactions on Software EngineeringFacilitating Mixed Language Programming in Distrbuted Systems
52 Citations1987Roger Hayes, Richard D. Schlichting
An approach for facilitating mixed language programming in distributed systems is presented, based on adding a generic remote procedure call facility to each language, and the use of a type system to describe procedural interfaces, as well as data to be transferred between procedures.
IEEE SoftwareGuest Editor's Introduction Multiparadigm Languages and Environments
45 Citations1986Brent Hailpern
Lecture notes in computer scienceViewPoint oriented software development: Methods and viewpoints in requirements engineering
39 Citations1991Anthony Finkelstein, Michael Goedicke +2 more
A central thread in this work the -concept of "ViewPoint"- is examined, motivated and systematically characterised, and the implications for methods to support the construction of formal specifications are considered.
Lecture notes in computer scienceTechniques for partial specification and specification of switching systems
24 Citations1991Pamela Zave, Michael Jackson
Lecture notes in computer scienceA case for structured analysis/formal design
19 Citations1991Nico Plat, J. van Katwijk +1 more
Two approaches to transforming data flow diagrams, the main system representation resulting from SA, to constructs in VDM are described and a comparison is made between the two presented models by analyzing their characteristics.
Towards Formalized Software Architectures
11 Citations1992Robert Allen, David Garlan
This work shows how a formal model allows us to say precisely what the authors mean by a software architecture, explore its properties, and systematically describe instances of the architecture.
Composition of Descriptions : A Progress Report
2 Citations1993Pamela Zave, Michael Jackson
This work has embarked upon an ambitious research project, and achieved some encouraging early results that will be presented in two forthcoming papers.
International Journal of Software Engineering and Knowledge EngineeringGUEST EDITORS' INTRODUCTION
2 Citations1992Bernd Krämer, M. Papazoglou