|
| Home > FAQ on different themes > |
| Larch Frequently Asked Questions (comp.specification.larch FAQ) |
Section 6 of 7 - Prev - Next
All sections - 1 - 2 - 3 - 4 - 5 - 6 - 7
program code was described with two predicates: a precondition and a
postcondition. Both the pre- and the postcondition were predicates on states
(that is, they can be considered functions that take a state and return a
boolean). The precondition described the pre-state; that is, it describes
the values of program variables just before the execution of a piece of
code. The postcondition described the post-state, which is the state after
the code's execution. In a Larch BISL the precondition is like this, but the
postcondition is typically a predicate on both the pre- and the post-state.
See section 4.8 What does ensures mean?, for more information.
4.8 What does ensures mean?
In most Larch BISLs, the keyword ensures introduces a postcondition into a
procedure specification. (This usage dates back to at least Larch/CLU
[Wing83].)
A postcondition in a Larch BISL is typically a predicate that is defined on
the pre-state and post-state of a procedure call. (See section 4.7 What does
requires mean?, for background and terminology.) It documents the
obligations of the called procedure in the contract that is being specified.
Therefore, it can be assumed to be true at the end of a call to the
procedure, when reasoning about the call.
As an example, consider the following specification of an integer swap
function which is to be written in C++ (this example is quoted from
[Leavens97]).
extern void swap(int& x, int& y) throw();
//@ behavior {
//@ requires assigned(x, pre) /\ assigned(y, pre);
//@ modifies x, y;
//@ ensures x' = y^ /\ y' = x^;
//@ }
In this specification, the parameters x and y are passed by reference, and
thus each is an alias for a variable in the caller's environment. Because x
and y denote variables, they can have different values in the pre-state and
the post-state. The postcondition of the example above says that the pre-
and post-state values of the variables x and y are exchanged. The notation
x^ refers to the value of x in the pre-state, and x' refers to its value in
the post-state. (This Larch/C++ notation is taken from LCL. In LM3 the ^
notation is not used. In Larch/Smalltalk, the ^ is likewise dropped, and a
subscript "post" is used instead of '.)
Depending on the particular BISL, a procedure specification may have one of
two different interpretations. In most Larch BISLs for sequential
programming languages, the interpretation is that if the precondition holds,
then the procedure must terminate normally in a state where the
postcondition holds. This is called a total correctness interpretation of a
procedure specification. In Hoare's original paper [Hoare69], and in GCIL
and Larch/CORBA, a partial correctness interpretation is used. This means
that if the precondition holds and if the procedure terminates normally,
then the postcondition must hold. You should check the documentation for
your BISL to be sure of its semantics on this point. (Larch/C++ is unique in
that it allows you to specify either interpretation; see [Leavens97],
Chapter 6).
4.9 What does modifies mean?
In most Larch BISLs, the keyword modifies introduces a list of objects that
can be modified by an execution of the specified procedure. (This usage
dates back to Larch/CLU [Wing83].)
An object is modified if its abstract value is changed by the execution of
the specified procedure. (That is, if it has a different abstract value in
the pre-state from the post-state.) Note that the modifies clause does not
mean that the execution must change the object's abstract values; it simply
gives the procedure permission to change them. For example, if a swap
procedure were passed variables with identical values (see section 4.8 What
does ensures mean?, for the specification of swap), then the values would
not be changed.
Note also that a variable's bits may change without a corresponding change
in abstract value (see section 4.4 What is an abstract value?). For example,
if one has a rational number object, whose representation uses two integers.
Let us write the two integers in the representation as (i,j); thus (2,4)
might be one bit pattern that represents the abstract value 1/2. However,
changing the bits from (2,4) to (1,2) would not affect the abstract value.
The modifies clause can be considered syntactic sugar for writing a larger
predicate in the postcondition. Since only the objects listed in the
modifies clause can have their abstract values changed by the execution of
the procedure, all other objects must retain their abstract values. There is
a problem in artificial intelligence called the "frame problem", which is
how to know that "nothing else has changed" when you make some changes to
the world. For this reason, the modifies clause in a Larch BISL can be said
to specify a frame axiom for the specified procedure. See [Borgida-etal95]
for a general discussion of the frame problem for procedure specifications.
In many specification languages, the frame axiom for a procedure
specification is stated in terms of variable names, but in Larch BISLs it is
typically stated in terms of objects. The difference is crucial when the
programming language allows aliasing. If the modifies clause in a Larch BISL
specified that only certain variable names could change their values, then
one would typically need to have either prohibit aliasing completely, or one
would need to write preconditions that prohibited aliases to variables that
were to be modified in procedures.
Mentioning an object in a modifies clause should not give the procedure
being specified permission to deallocate the object. If that were allowed,
it would lead to problems in the BISL's semantics [Chalin95]
[Chalin-etal96]. See section 4.10 What does trashes mean?, for more
information on this topic.
4.10 What does trashes mean?
A trashes clause is similar to a modifies clause (see section 4.9 What does
modifies mean?) in a procedure specification. It gives the procedure
permission to deallocate or trash the objects listed. These objects do not
have to be deallocated or trashed, but no other objects may be deallocated
or trashed.
The notion of trashing an object means that its abstract value should not be
used again. In Larch/C++, allocated variables can be in one of two states:
assigned or unassigned; a variable is unassigned if it has not been assigned
a sensible value. However, if one assigns to an assigned variable, a, the
value of an unassigned variable, then a becomes unassigned, and hence is
considered to be trashed.
Chalin [Chalin95] [Chalin-etal96] pointed out that specification of what a
procedure can modify should be separated from the specification of what it
can deallocate or trash. When these notions are separated, as they are in
Larch/C++ (see [Leavens97], chapter 6), there are two frame axioms for
procedure specifications.
An alternative to a trashes clause, used in LCL, is to specify input/output
modes for formal parameters [Evans00]. Some parameter modes do not allow
trashing, and some do not allow modification.
4.11 What does claims mean?
The claims clause, and other kinds of checkable redundancy for BISLs, were
introduced into LCL by Tan [Tan94]. In a procedure specification, the
keyword claims introduces a predicate, called a claim, that, like the
postcondition, relates the pre- and post-states of a procedure's execution.
Roughly speaking, the meaning is that the conjunction of the precondition
and the post condition should imply the claim. This implication can be
checked, for example, by using LP.
You could use the claims clause if you wish to highlight some consequences
of your procedure specification for the reader. It can also be used to help
debug your understanding of a procedure specification; for example, if you
think of more than one way to express a postcondition, write all but one way
in a claims clause. Thus the purpose of this clause is similar to the
purpose of the implies section of an LSL trait (see section 2.11 When should
I use an implies section?).
4.12 What is the meaning of a specification written in a BISL?
The exact meaning of a specification in a BISL is, of course, described by
the reference manual for that particular BISL. But in general, the meaning
of a BISL specification is a set of program modules that satisfy the
specification. These program modules are to be written in the programming
language specified. For example, the meaning of a LCL specification is a set
of ANSI C program modules that satisfy the specification. Similarly, the
meaning of a Larch/C++ specification is a set of C++ program modules that
satisfy the specification; a Larch/C++ specification cannot be implemented
in, say, Ada or Modula-3.
How does one describe the satisfaction relation for a BISL? Suppose you want
to describe satisfaction for the BISL Larch/X, whose programs are to be
written in language X. Then you describe the satisfaction relation in at
least the following ways.
* Give a semantics for language X, that assigns to each program module,
P, a meaning, M(P). Describe, for each specification, S, written in
Larch/X, when M(P) is in the set of meanings specified by S.
* Develop a verification logic for language X, that says how to check
that code satisfies a specification (or some other specification). Then
a program module P satisfies a specification S if one can use the
verification logic to check that P satisfies S.
The first technique will probably allow more programs, in principle, to
satisfy the specification, especially if the semantics of language X covers
all aspects of the language. The second technique is probably more limiting,
but is certainly more useful in practice. These techniques are not mutually
exclusive; for example, a relatively complete verification logic could be
used as a semantics for that language. Furthermore, by using complimentary
definitions of the programming language (e.g., a denotational semantics and
a verification logic), one could prove soundness and completeness results,
which would help debug each kind of semantics, and thus the semantics of the
BISL as well.
See [Wing83] for a semantics of Larch/CLU. See [Jones93] for a semantics of
LM3. See [Tan94] [Chalin95] for semantics of LCL.
4.13 How do I specify something that is finite or partial?
In a procedure specification, you would normally use a precondition to limit
the acceptable arguments that the procedure can work with. For example, the
standard LSL handbook trait Integer (see [Guttag-Horning93], page 163)
specifies an unbounded set of integers. Many Larch BISLs use this kind of
unbounded set of integers as their model of a programming language's
built-in integer type. Suppose that you want to specify an integer
discriminant function, say to be implemented in C++. In Larch/C++ you could
specify this as follows.
extern int discriminant (int a, int b, int c) throw();
//@ behavior {
//@ requires inRange((b * b) - (4 * a * c));
//@ ensures result = (b * b) - (4 * a * c);
//@ }
Notice the precondition; it says that the result must be able to be
represented as an int in the computer (according to the definition of the
operator inRange, which is defined in a built-in trait of Larch/C++
[Leavens97]). Without this precondition, the specification could not be
implemented, because if b were the maximum representable integer, and if a
and c were 0, then the specification without the precondition would say that
the execution would have to terminate normally and return an integer larger
than the maximum representable integer.
(The specification of descriminant above may not be the best design for the
procedure, because it requires a precondition that is difficult to test
without performing the computation specified. See section 4.17 Can you give
me some tips for specifying things in a BISL?, for more discussion of this
point.)
The idea of using preconditions to get around partiality and finiteness
problems in procedures goes back to Hoare's original paper on program
verification [Hoare69].
To specify an ADT with a finite set of values, such as a bounded queue, use
a trait with unbounded values to specify the abstract values. You can then
use an invariant in the BISL specification of your ADT to state that the
size of the abstract values is limited. Most likely the ADT operations that
construct and mutate objects would need to have preconditions that prevent
the abstract value from growing too large. This approach is preferred over
an approach that specifies a finite set of abstract values in LSL, because
that trait would be more complicated and less likely to be able to be reused
(see section 2.20 How do I know when my trait is abstract enough?). Even
with such a trait, you would still need to have preconditions on your
operations that construct and mutate objects, so there is little gained.
4.14 How do I specify errors or error-checking?
Ways of specifying errors and error checking vary between Larch BISLs,
depending primarily on whether the programming language that the BISL is
tailored to has exceptions. In a language without exceptions (like ANSI C),
a procedure would have to signal an error by producing an error message and
halting the program, or by returning some error indication to the caller of
a procedure. If you want to specify that the program halts, most likey you
will just not include the conditions under which it can do so in your
precondition (see section 4.13 How do I specify something that is finite or
partial?). If you want to specify the returning of some error indication (a
return code, etc.), this is done as if you were specifying any other normal
result of a procedure. In a language with exceptions (like C++), there is
the additional option of using the exception handling mechanism to signal
errors to the caller. The syntax of this varies, but typically you will
declare the exceptions as usual for the programming language, and there will
be some special way to indicate in the postcondition that an exception is to
be raised.
Many Larch BISLs (including LCL, LM3, Larch/Ada, and Larch/C++) have special
syntax to support the specification of error checking and signalling
exceptions. However, there is little common agreement among the various
Larch BISLs on the syntax for doing so; please check the manual for your
particular BISL. (See section 1.1 What is Larch? What is the Larch family of
specification languages?, for how to find your language manual.)
See [Liskov-Guttag86] for a discussion of the tradeoffs between using
preconditions and various kinds of defensive programming.
4.15 How do I specify that all the values of a type satisfy some property?
A property that is true for all values of a type is called an invariant.
Many Larch BISLs have syntax for declaring invariants. For example, LM3 uses
the keyword TYPE_INVARIANT, and Larch/C++ uses the keyword invariant. The
predicate following the appropriate keyword has to hold for all objects
having that type, whenever a client-visible operation of that type is called
or returns. (This allows the invariant to be violated temporarily within an
operation implementation.)
Stating an invariant in the BISL specification of an ADT is often preferable
to designing an LSL trait so that the abstract values all satisfy the
property. For example, if you attempt to state such a property as an axiom
in a trait, you can cause the trait to be inconsistent, if the abstract
values of your type are freely generated (see section 2.18 What pitfalls are
there for LSL specifiers?). But invariants in a BISL do not lead to such
inconsistencies, because they describe properties of objects created by an
ADT, not properties of all abstract values.
See section 4.13 How do I specify something that is finite or partial?, for
more discussion about ways to specify that all values of an ADT are finite.
4.16 What pitfalls are there for BISL specifiers?
The main thing to watch out for in a BISL specification is that you don't
specify something that cannot be implemented. It's worth repeating the
following mantra to yourself whenever you write a procedure specification.
Could I correctly implement that?
Of course, you would never intentionally specify a procedure that cannot be
implemented. So you are only likely to fall into this pit by accident. The
following are some ways it might happen.
A very simple problem is forgetting to write a modifies (or trashes) clause
in a procedure specification when your postcondition calls for some object
to change state (or be deallocated). Remember that leaving out a modifies
clause means that no objects can be modified. Consider the following bad
specification of an increment procedure in Larch/C++. (The formal parameter
i is passed by reference. The throw() says that no exceptions can be thrown.
In the precondition, the term assigned(i, pre) is a technical detail; it
says that i has been previously assigned a value [Leavens97].)
extern void incBad(int& i) throw();
//@ behavior {
//@ requires assigned(i, pre);
//@ ensures i' = i^ + 1;
//@ }
There can be no correct implementation of the above specification, because
the omitted modifies clause does not allow i to be modified, but the
postcondition guarantees that it will be modified. This contradiction
prevents correct implementations.
A more subtle way that your specification might not be implementable is if
you forget to specify a necessary precondition. Suppose we fix the above
specification and produce the following specification of an increment
function. What's wrong now?
extern void incStillBad(int& i) throw();
//@ behavior {
//@ requires assigned(i, pre);
//@ modifies i;
//@ ensures i' = i^ + 1;
//@ }
This specification can't be implemented, because if the pre-state value of i
is the largest int, INT_MAX, then the value INT_MAX+1 can't be stored in it.
So, as specified, there are no correct implementations. Something has to be
done to accommodate the finite range of integers that can be stored in i.
Changing the precondition to be the following would take care of the
problem.
assigned(i, pre) /\ i^ < INT_MAX
In summary, one thing to watch for is whether you have taken finiteness into
account. See section 4.13 How do I specify something that is finite or
partial?, for more about finiteness considerations in BISL specifications.
Another way that your specification might be unimplementable is if your
stated postcondition contradicts some invariant property (see section 4.15
How do I specify that all the values of a type satisfy some property?) that
you specified elsewhere.
The following is another Larch/C++ example. The term inRange(e), used in the
precondition, means that e is within the range of representable integer
values, hence the specification takes finiteness into account. What else
could be wrong with the specification?
extern void transfer(int& source, int& sink, int amt);
//@ behavior {
//@ requires assigned(source, pre) /\ assigned(sink, pre) /\ amt >= 0
//@ /\ inRange(source^ - amt) /\ inRange(sink^ + amt);
//@ modifies source, sink;
//@ ensures source' = source^ - amt /\ sink' = sink^ + amt;
//@ }
The above specification can't be implemented because it doesn't require that
source and sink not be aliased. Since both source and sink are passed by
reference, suppose that both refer to the same variable i. Then if amt is
nonzero, the postcondition cannot be satisfied. (Suppose the pre-state value
of i is 10, and that amt is 5, then the post-state must satisfy source' = 10
- 5 /\ sink' = 10 + 5, but since both source and sink are aliases for i,
this would require that i' be both 5 and 15, which is impossible.) In
Larch/C++, this could be fixed by adding the following conjunct to the
precondition, which requires that source and sink not be aliased.
source ~= sink
Some Larch BISLs (e.g., Larch/Ada) prohibit aliasing in client programs, so
if you are using such a BISL, then you don't have to worry about this
particular way of falling in the pit. But if your BISL does not prohibit
aliasing, then you should think about aliasing whenever you are dealing with
mutable objects or call-by-reference.
4.17 Can you give me some tips for specifying things in a BISL?
A basic tip for writing a BISL specification is to try to permit as many
implementations as possible. That is, you want to specify a contract between
clients and implementors that does everything the client needs, but does not
impose any unneeded restrictions on the implementation.
One thing that experienced specifiers think about is whether the
specification permits implementations to be tested. This is particularly
important for preconditions. For example, when specifying an ADT, check that
the ADT has enough operations to allow the pre- and postconditions specified
to be tested. If you specify a Stack ADT but leave out a test for the empty
stack, then it will be impossible for a client to test the precondition of
the pop operation. (However, there are some rare examples, such as a
statistical database, where you might not want to allow clients to have such
access.)
If implementations can be tested, it is often useful to compare the
difficulty in testing the specified precondition with the difficulty of
doing the specified computation. For example, in the specification of
discriminant (see section 4.13 How do I specify something that is finite or
partial?), checking the precondition is likely to be as difficult as the
specified computation. In such a case, it may be wise to change the
specification by weakening the precondition and allowing the procedure to
signal some kind of error or exception.
Another tip is to try to use names for operators in traits that are distinct
from the name of the procedure you are trying to specify (or vice versa).
For example, the casual reader might incorrectly think that the following
specification is recursive.
//@ uses FooTrait;
extern int foo(int input);
//@ behavior {
//@ ensures result = foo(input);
//@ }
There is no logical problem with the above example, since the operators used
in a postcondition cannot have anything to do with the interface procedure
being specified. However, naive readers of specifications are (in our
experience) sometimes confused by such details.
See section 4.16 What pitfalls are there for BISL specifiers?, for pitfalls
to avoid. See [Liskov-Guttag86] [Meyer97] [Meyer92] for general advice on
designing and specifying software. See [Wing95] for some other tips on
formal specification.
Bibliography
Please send corrections in this bibliography to
larch-faq@cs-DOT-iastate-DOT-edu.
[Baraona-Alexander-Wilsey96]
Phillip Baraona, Perry Alexander, and Philip A. Wilsey. Representing
Abstract Architectures with Axiomatic Specifications and Activation
Conditions. Department of Electrical and Computer Engineering and
Computer Science, PO Box 210030, The University of Cincinnati,
Cincinnati, OH, April 1996. Available from the URL
`http://www.ece.uc.edu/~pbaraona/vspec/papers/fmcad96.ps'.
[Baraona-Alexander96]
Phillip Baraona and Perry Alexander. Abstract Architecture
Representation Using VSPEC. Department of Electrical and Computer
Engineering and Computer Science, PO Box 210030, The University of
Cincinnati, Cincinnati, OH, April 1996. Available from the URL
`http://www.ece.uc.edu/~pbaraona/vspec/papers/vspec-arch96.ps'.
[Baraona-Penix-Alexander95]
Phillip Baraona, John Penix, and Perry Alexander. VSPEC: A Declarative
Requirements Specification Language for VHDL. In J. M. Berge, O. Levia,
and J. Rouilard (eds.), High-Level System Modeling: Specification
Languages, pages 51-75. Volume 3 of Current Issues in Electronic
Modeling (Kluwer Academic Publishers, June 1995).
[Baumeister96]
Hubert Baumeister. Using Algebraic Specification Languages for
Model-Oriented Specifications. Technical Report MPI-I-96-2-003,
Max-Planck-Institut fuer Informatik, February 1996. Available from the
URL
`http://www.mpi-sb.mpg.de/~hubert/MPII-96-2-003.html'.
[Borgida-etal95]
Alex Borgida, John Mylopoulos, and Raymond Reiter. On the Frame Problem
in Procedure Specifications. IEEE Transactions on Software Engineering,
21(10):785-798, October 1995.
[Bowen-Hinchey95]
J. P. Bowen and M. G. Hinchey. Seven More Myths of Formal Methods. IEEE
Software, 12(4):34-41 (July 1995).
[Bowen-Hinchey95b]
J. P. Bowen and M. G. Hinchey. Ten Commandments of Formal Methods. IEEE
Computer, 28(4):56-63 (April 1995).
[Boyer-Moore79]
Robert S. Boyer and J Strother Moore. A Computational Logic. Academic
Press, 1979.
[Boyer-Moore88]
Robert S. Boyer and J Strother Moore. A Computational Logic Handbook.
Academic Press, 1988.
[Chalin95]
Patrice Chalin. On the Language Design and Semantic Foundation of LCL,
a Larch/C Interface Specification Language. PhD thesis, Computer
Science Department, Concordia University, October 1995. Also Technical
Report CU/DCS TR 95-12, which can be obtained from the URL
`ftp://ftp.cs.concordia.ca/pub/chalin/tr.ps.Z'.
[Chalin-etal96]
Patrice Chalin, Peter Grogono, and T. Radhakrishnan. Identification of
and solutions to shortcomings of LCL, a Larch/C interface specification
language. In Marie-Claude Gaudel and James Woodcock (eds.), FME'96:
Industrial Benefit and Advances in Formal Methods, pages 385-404.
Volume 1051 of Lecture Notes in Computer Science, Springer-Verlag,
1996. See also CU/DCS TR 95-04, which can be obtained from the URL
`ftp://ftp.cs.concordia.ca/pub/chalin/CU-DCS-TR-95-04.ps.Z'.
[Chen89]
Jolly Chen. The Larch/Generic Interface Language. Bachelor's thesis,
Massachusetts Institute of Technology, EECS department, May, 1989.
(Available from John Guttag: guttag@lcs.mit.edu.)
[Cheon-Leavens94]
Yoonsik Cheon and Gary T. Leavens. The Larch/Smalltalk Interface
Specification Language ACM Transactions on Software Engineering and
Methodology, 3(3):221-253 (July 1994).
[Cheon-Leavens94b]
Yoonsik Cheon and Gary T. Leavens. A Gentle Introduction to
Larch/Smalltalk Specification Browsers. Department of Computer Science,
Iowa State University, TR #94-01, January 1994. Available from the URL
`ftp://ftp.cs.iastate.edu/pub/techreports/TR94-01/TR.ps.Z'.
[Chetali98]
Boutheina Chetali. Formal Verification of Concurrent Programs Using the
Larch Prover. IEEE Transactions on Software Engineering, 24(1):46-62
(Jan., 1998).
[DeMillo-Lipton79]
Richard A. De Millo and Richard J. Lipton and Alan J. Perlis. Social
Processes and Proofs of Theorems and Programs. Communications of the
ACM, 22(5):271-280 (May 1979).
[Edwards-etal94]
Stephen H. Edwards, Wayne D. Heym, Timothy J. Long, Murali Sitaraman,
and Bruce W. Weide. Part II: Specifying Components in RESOLVE. ACM
SIGSOFT Software Engineering Notes, 19(4):29-39 (Oct. 1994).
[Ehrig-Mahr85]
Hartmut Ehrig and Bernd Mahr. Fundamentals of Algebraic Specification
1: Equations and Initial Semantics. EATCS Monographs on Theoretical
Computer Science, volume 6 (Springer-Verlag, NY, 1985).
[Evans00]
David Evans. LCLint User's Guide, Version 2.5, May 2000. Available at
the following URL `http://lclint.cs.virginia.edu/guide/'.
[Feijs-Jonkers92]
L. M. G. Feijs and H. B. M. Jonkers. Formal Specification and Design.
Volume 35 of Cambridge Tracts in Theoretical Computer Science
(Cambridge University Press, Cambridge, UK, 1992).
[Fetzer88]
James H. Fetzer. Program Verification: The Very Idea. Communications of
the ACM, 31(9):1048-1063 (Sept. 1988).
[Finney96]
Kate Finney. Mathematical Notation in Formal Specifications: Too
Difficult for the Masses? IEEE Transactions on Software Engineering,
22(2):158-159 (February 1996).
[Fitzgerald-Larsen98]
John Fitzgerald and Peter Gorm Larsen Modelling Systems: practical
tools and techniques in software development. Cambridge University
Press, 1998.
[Futatsugi-etal85]
Kokichi Futatsugi, Joseph A. Goguen, Jean-Pierre Jouannaud, and Jose
Meseguer. Principles of OBJ2. In Conference Record of the Twelfth
Annual ACM Symposium on Principles of Programming Languages, pages
52-66 (ACM, January 1985).
[Garland-Guttag91]
S. J. Garland and J. V. Guttag. A Guide to LP, The Larch Prover.
Technical Report 82, Digital Equipment Corp, Systems Research Center,
130 Lytton Avenue Palo Alto, CA 94301, December, 1991. This is
superseded by [Garland-Guttag95].
[Garland-Guttag-Horning90]
Stephen J. Garland, John V. Guttag, and James J. Horning. Debugging
Larch Shared Language Specifications. IEEE Transactions on Software
Engineering, 16(6):1044-1057 (Sept. 1990). Superseded by Chapter 7 in
[Guttag-Horning93].
[Garland-Guttag95]
Stephen J. Garland and John V. Guttag. LP, the Larch Prover. On-line
documentation for release 3.1a (MIT Laboratory for Computer Science,
April 1995). Available in the LP distribution and from the URL
`http://www.sds.lcs.mit.edu/spd/larch/LP/contents.html'.
[Goguen-etal87]
J. Goguen, C. Kirchner, A. Megrelis, J. Meseguer, and T. Winkler. An
Introduction to OBJ3. In S. Kaplan and J.-P. Jouannaud (eds.),
Conditional Term Rewriting Systems, 1st International Workshop, Orsay,
France, pages 258-263. Lecture Notes in Computer Science, Volume 308
(Springer-Verlag, NY, 1987).
[Goguen-Thatcher-Wagner78]
J. A. Goguen, J. W. Thatcher, and E. G. Wagner. An Initial Algebra
Approach to the Specification, Correctness and Implementation of
Abstract Data Types. In Raymond T. Yeh (ed.), Current Trends in
Programming Methodology, volume 4, pages 80-149 (Prentice-Hall,
Englewood Cliffs, N.J., 1978).
[Goguen84]
J. A. Goguen. Parameterized Programming. IEEE Transactions on Software
Engineering, SE-10(5):528-543 (Sept. 1984).
[Goguen86]
J. A. Goguen. Reusing and Interconnecting Software Components IEEE
Computer, 19(2):16-28 (February 1986).
[Gordon-Melham93]
M. J. C. Gordon and T. F. Melham. Introduction to HOL: A Theorem
Proving Environment for Higher Order Logic. Cambridge University Press,
1993.
[Gries-Schneider95]
David Gries and Fred B. Schneider. Avoiding the Undefined by
Underspecification. In Jan van Leeuwen (ed.), Computer Science Today:
Recent Trends and Developments, pages 366-373. Volume 1000 of Lecture
Notes in Computer Science (Springer-Verlag, NY, 1995).
[Guaspari-Marceau-Polak90]
David Guaspari, Carla Marceau, and Wolfgang Polak. Formal Verification
of Ada Programs. IEEE Transactions on Software Engineering,
16(9):1058-1075 (Sept. 1990). Reprinted in [Martin-Wing93], pages
104-141.
[Guttag-Horning-Modet90]
John V. Guttag, J. J. Horning, and Andres Modet. Report on the Larch
Shared Language: Version 2.3. Technical Report 58, Digital Equipment
Corp, Systems Research Center, 130 Lytton Avenue Palo Alto, CA 94301,
April, 1990. Order from src-report@src.dec.com or from the URL
`http://www.research.digital.com/SRC/publications/src-rr.html'.
[Guttag-Horning-Wing85a]
J. V. Guttag, J. J. Horning, and J. M. Wing. Larch in Five Easy Pieces.
Technical Report 5, Digital Equipment Corp, Systems Research Center,
130 Lytton Avenue Palo Alto, CA 94301, July 1985. Superseded by
[Guttag-Horning93].
[Guttag-Horning-Wing85b]
John V. Guttag, James J. Horning and Jeannette M. Wing. The Larch
Family of Specification Languages. IEEE Software, 2(5):24-36 (Sept.
1985).
[Guttag-Horning78]
J. V. Guttag and J. J. Horning. The Algebraic Specification of Abstract
Data Types. Acta Informatica, 10(1):27-52 (1978).
[Guttag-Horning91b]
J. V. Guttag and J. J. Horning. A Tutorial on Larch and LCL, a Larch/C
Interface Language. In S. Prehn and W. J. Toetenel (eds.), VDM '91
Section 6 of 7 - Prev - Next
All sections - 1 - 2 - 3 - 4 - 5 - 6 - 7
| Back to category FAQ on different themes - Discuss "Larch Frequently Asked Questions (comp.specification.larch FAQ)" |
| Home - Search - About the project - Forum - Feedback |
© allanswers.org | Terms of use