# Larch: Languages and Tools for Formal Specification

@inproceedings{Guttag1993LarchLA, title={Larch: Languages and Tools for Formal Specification}, author={John V. Guttag and James J. Horning and Stephen J. Garland and Kevin D. Jones and A. Modet and Jeannette M. Wing}, booktitle={Texts and Monographs in Computer Science}, year={1993} }

This monograph addresses the use of formal specification languages and supporting tools. Concentrating on the Larch specification work taking place at DEC and MIT, it discusses the use of formal specifications in program development and introduces the notation of mathematical logic.

#### Figures and Topics from this paper

#### 820 Citations

Comparison of the Formal Specification Languages Based Upon Various Parameters

- Computer Science
- 2013

This paper describes how a particular specification language is used for a specific problem and a comparison of different formal specification languages is done taking various parameters. Expand

Formal specification of concurrent systems

- Computer Science
- 1999

A refinement strategy that relates an implementation in a programming language to a formal specification of such a system and illustrates the methodology on an example that uses the preconditioned conjugate gradient method for solving a linear system of equations. Expand

Reasoning with Executable Specifications

- Computer Science
- TAPSOFT
- 1995

This work formally proves the correctness of two program transformations on a small imperative programming language, given in a single format, that can be compiled into both executable tools and collections of definitions to reason about into a theorem prover. Expand

An Architecture for Interactive Program Provers

- Computer Science
- TACAS
- 2000

The modular architecture of an interactive program prover that is currently developing for a Java subset is described, which discusses the integration of a programming language-specific prover component with a general purpose theorem prover. Expand

Semantic analysis of Larch Interface Specifications

- Computer Science
- Larch
- 1992

Claims can be used to debug formal specifications, help readers better understand a formal specification, highlight important features of a software design, support program verification, and help generate test cases. Expand

Reflections on the Design of a Specification language

- Computer Science
- FASE
- 1998

We reflect on our experiences from work on the design and semantic underpinnings of Extended ML, a specification language which supports the specification and formal development of Standard ML… Expand

A Semantics for a Larch/Modula-3 Interface Language

- Computer Science
- Larch
- 1992

We describe a method for giving a semantics to a Larch interface language specification by a translation of the specification into typed first-order logic. This is illustrated using LM3, a… Expand

Testing Implementations of Algebraic Specifications with Design-by-Contract Tools

- Computer Science
- 2005

An approach for testing Java implementations of abstract data types (ADTs) against their specifications is presented, which comprises an ADT specification language that allows automatic generation of monitorable contracts and a refinement language that supports the specification of the details of object-oriented implementations of ADTs. Expand

Essential concepts of algebraic specification and program development

- Mathematics, Computer Science
- Formal Aspects of Computing
- 2005

The main ideas underlying work on the model-theoretic foundations of algebraic specification and formal program development are presented in an informal way to offer an overall view and to focus on the basic motivation behind the technicalities presented elsewhere. Expand

Formal semantics of an algorithm for translating model-based specifications to concurrent constraint programs

- Computer Science
- SAC
- 2001

The semantics of the algorithm for executing formal speci cations written at a high level of abstraction and provides the basis for a soundness proof. Expand

#### References

SHOWING 1-10 OF 91 REFERENCES

Semantic analysis of Larch Interface Specifications

- Computer Science
- Larch
- 1992

Claims can be used to debug formal specifications, help readers better understand a formal specification, highlight important features of a software design, support program verification, and help generate test cases. Expand

The Semantics of CLEAR, A Specification Language

- Computer Science
- Abstract Software Specifications
- 1979

A blend of denotational semantics with categorical ideas is used for the Clear language for specifying problems and programs, described by Burstall and Goguen in 1977. Expand

A Semantics for a Larch/Modula-3 Interface Language

- Computer Science
- Larch
- 1992

We describe a method for giving a semantics to a Larch interface language specification by a translation of the specification into typed first-order logic. This is illustrated using LM3, a… Expand

The Larch Family of Specification Languages

- Computer Science
- IEEE Software
- 1985

Larch specifications are two-tiered. Each one has a component written in an algebraic language and another tailored to a programming language.

Formal specification as a design tool

- Computer Science
- POPL '80
- 1980

This paper outlines a specification language combining algebraic axioms and predicate transformers, presents part of a non-trivial example (the specification of a high-level interface to a display), and discusses the analysis of this specification. Expand

Optimizing Programs with Partial Specifications

- Computer Science
- Larch
- 1992

A compilation method that exploits formal specifications to optimize programs that are impossible using techniques based purely on code analysis because formal specifications contain information that cannot be deduced from code. Expand

Synchronization primitives for a multiprocessor: a formal specification

- Computer Science
- SOSP '87
- 1987

This work presents a way to formally specify interfaces in concurrent systems, gives a formal specification of the synchronization primitives of the Taos operating system, and discusses the implementation of the specification. Expand

Writing Larch interface language specifications

- Computer Science
- TOPL
- 1987

This paper gives an example of writing an interface specification following the two-tiered approach to writing specifications and discusses in detail issues involved in writing interface specifications and their interaction with their Shared Language components. Expand

A TWO-TIERED APPROACH TO SPECIFYING PROGRAMS

- Computer Science
- 1983

This thesis presents an interface specification language for the CLU programming language and presumes the use of the Larch shared language, and suggests a number of kinds of analyses that one might want to perform on two-tiered specifications. Expand

The DECspec project: tools for Larch/C

- Computer Science
- [1992] Proceedings of the Fifth International Workshop on Computer-Aided Software Engineering
- 1992

The DECspec project was inaugurated to explore the application of formal methods in a production environment and the Larch formal specification method was selected, with C as the target programming language. Expand