[Prev][Next][Index]
Survey Results
Dear Larch-Interest People:
First, I would like to thank everyone who responded to my survey. I
got 43 responses out of the 66 names (of people) on larch-interest.
It was fascinating reading your answers to my questions. I was
impressed with the general level of enthusiasm and interest by the
Larch users, even though we're a small community. We are also a
demanding community (see the wish list).
I've collated the results, which I've appended below. It's 16 pages
of unformatted ASCII text. I may have erred on the side of including
too much information but I thought you might be interested in seeing
people's specific responses rather than my condensation of them.
Also, I didn't want to be very fancy and do any kind of statistical
analysis or correlations. Editorial comments are in square brackets.
Given your interests and wish lists, there are a few obvious bridges
to build so I've put names and e-mail addresses of some people under
responses to Question 7. If you're one of them, I hope this is okay
with you.
Check out the humor page at the end.
Jeannette Wing
========================Survey Results==============================
1. Administrative Data
People on larch-interest list 66
People responding to survey 43 (65%)
Faculty 12
Grad Students 13
Industrial Researchers 9
Software Engineers 9
Research Interests:
[I counted you once for each category you gave, whether general or
specific.]
Formal methods 11
Formal specification 7
Module interface
specification languages 1
Algebraic specs 4
(including equational theories, rewriting)
Spec environments 2
Formal verification 3
Hardware 2
Software 4
(compilers, programs, ADTS)
Software engineering 10
(design (1), testing (1), prototyping (1),
reengineering (1), environments (2))
Programming methodology 4
Distributed 6
(programming, languages and systems)
Parallel/concurrent 4
(programming, languages, and systems
Languages 9
(design, implementation, semantics)
Object-oriented 5
(programming, languages, databases, semantics)
Functional 3
(programming, languages, semantics)
Theorem proving 2
Other (1 each)
UI, applications of connected computing, high-level circuit design,
tractable analysis, architectures (SW & HW) for real-time
image understanding, heterogeneous computing, FSTs,
computers in education, programming without programming languages,
information processing/filtering.
2. Why are you interested in Larch? Why do you subscribe to the
larch-interest mailing list?
[I moved some specific quotes in response to this question to
Question 5, "Why I like Larch?"]
Interest in formal methods for software development 11
Teach a course on formal methods in sw eng. 4
Two-tiered approach 5
Approach is logical, practical, simple, useful 2
Close to code-level, takes programs seriously, 3
gets you down to code
Languages 6
Tools (in general) 7
LP (specifically mentioned) 6
Clarity in documentation 2
Semantics 1
Historical 4
Other (1 each)
-helped develop it
-possibilities it offers for static code checking,
-technology transfer
-studying pragmatic forms of behaviour specification to
allow the reasoning on the OO subtype relation behavioural compability.
-writing a book comparing a variety of specification methods,
among them Larch.
3. How do you USE Larch?
[A few people who replied used to use the languages or tools;
about the same number said they were planning to use them. I've
include past, current, and future users in these numbers.]
a. I use the following Larch LANGUAGES (check all that apply):
LSL (Larch Shared Language) 24
LCL (Larch/C Interface Language) 17
LM3 (Larch/Modula-3 Interface Language) 4
Larch/Ada 2
Larch/Smalltalk 2
Larch/C++ 7
GCIL (Larch Generic Concurrent Interface Language) 3
Larch/VHDL 1
Larch/CORBA 1
Speckle 1
ML (future) 1
b. I use the languages for specifying problems in the following
DOMAINS and/or EXAMPLES (fill in blank space with
a short description of your problem domains, case studies, etc.):
Used LCL and LSL to encode the semantics of LCL (in a fashion similar to Tan).
I use Larch as a formal design language (not as a reqs
specification language; for this we use Z). We use it in the design
phase; some examples: a chess editor/database and a distributed
multiuser service.
Case studies for using LCLint, also specifying LCLint sourcecode.
I have been using LSL to formalize properties of concurrent
algorithms in terms of Nancy Lynch's notion of input/output
automata.
Financial software. Preparing input for LP.
GUIs, databases, synchronization primitives, Modula-3 standard interfaces
ADT and window widgets.
I am trying to find a way to transform restricted Oberon programs into an
LSL trait. The resulting trait together with a trait specifing a
representation function from the abstract to the concrete type are
then proved to imply the axioms of a LSL specification of the
implemented abstract data type.
Using LCL, I specified and described the key modules of an existing,
working, 1800-line C program. The program keeps track of the
portfolio of an investor. It processes a sequence of financial
security transactions, checks their consistency, and summarizes the
portfolio. It handles stocks, bonds, options, Treasury bills, and
cash transactions [1] [See reference at end of survey.]
Specifying interfaces of program modules, typically library-level interfaces.
Domain: Communication protocol development systems;
Case study : Specify the x-kernel.
Have used it for pieces of a distributed operating system kernel,
for lots of toy examples, for the logic of the interface to a flight
controller.
Distributed building access control systems; Point Of Sale
transaction monitoring; embedded event-driven systems
Open, Distributed Applications.
Distributed systems, database systems....
Distributed systems.
c. I use the following Larch TOOLS (check all that apply):
LSL checker 21
LCL checker 10
LCLint 8
LP 26
Penelope 1
Old LSL syntax-directed editor 1
d. I use LP for specifying/proving properties in the following
DOMAINS and/or EXAMPLES (fill in blank space with
a short description of your problem domains, case studies, etc.):
Formal verification of circuits :
- Proof of the equivalence between an implementation and a specification
- Proof of invariants
- Proof of characteristic properties of circuits
Compiler verification, modelling semantics definitions, proving
properties about these
Reasoning about concurrency and circuits. [See References at end of survey.]
Circuits, distributed algorithms and protocols
Relational arithmetic (relations plus division and roots of relational
equations)
Hardware specification and verification
As a back end for the TLP verification system.
Examples in UNITY (done by Boutheina Chetali)
Refinement of hardware design descriptions.
I used LP to verify some properties (LCL claims) about the
specifications of the portfolio manager program indicated in (3b) in
order to help test the specification [1]. [See reference at
end of survey.]
Proving that a predicate holds a some point in a program.
We test properties of the design in the large. Examples:
a chess editor/database and a distributed multiuser service.
Test cases for algebraic spec. languages: Data Structures, Transit-Node
Distributed systems
e. I TEACH Larch (check all that apply):
[] in an undergraduate course
software engineering 3
formal methods (including just one lecture) 4
programming with Modula-3 1
[] in a graduate course
software engineering 1
formal methods 1
[] other
two-day LP course 1
4. Larch WISH list. What additional or improved support for Larch would you
like to see?
Tool support for
================
Modula-3 !!!!!
An LCLint for a Larch/C++
LM3
Tractable, approximate proofs
Fuller integration of LSL and LCL with LP
PC support: Linux, MSWindows. I understand that Linux is
supported, although it is not one of the standard platforms.
Verification of implementations with respect to a certain LSL trait
A tool to help create/edit/maintain Larch specifications. The tool
should understand at least some parts of the spec (for purposes like:
'Get me all the LSL traits used by the specification' automatically.
The tool should maintain a library of existing specifications (like
all those LSL traits in the LSL handbook).
Refinement of specifications, eventually down to implementation
Literate programming tool
Improvements to existing tools
==============================
LSL checker
----------
Better diagnostics. Even simple syntax errors can be difficult identify.
Subtyping, full first order
Integration with LP
LCL checker
-----------
Better diagnostics. Even simple syntax errors can be difficult identify.
LCLint
------
Lots of things described in my thesis (SM thesis entitled
"Using Specifications to Check Source Code" (available as a TR soon)).
[Contact: David Evans, evs@sds.lcs.mit.edu]
Better dependency analysis
Extension to LC++Lint
LP
--
Conditional rewriting
An easy way to implement strategies/tactics/whatever you want to call it
Support for more than 40 MB of memory (it simply doesn't work here!)
The suffixes that are generated for names of LP objects keep being
incremented even if parts of proofs are cancelled. Sometimes this
makes proving more complicated than necessary. I think it shouldn't
be too complicated to include the current index counter in the state
that is restored after a cancel command.
The names of objects that are generated during a proof are not
always chosen in a way that makes it easy to guess their type, in
particular if there are many sorts around with a lot of different
variables declared for them. I think it would be a good idea to let
the user declare a standard prefix for names of new objects of the
several sorts.
Better proof and theory management, fast special purpose
procedures for propositional logic, arithmetic, and set theory
Tactics, proof management
Lambda abstraction
Support for quantifiers
Better decision procedures for integers/natural numbers
More documented case studies
============================
Real cases where people use Larch tools to develop or maintain
software. "Fabricated" case studies are useful, but cases where
someone is using Larch tools for a project not for the sake of testing
the tools, but to aid the project would be most telling.
Any kind [2 votes for this!]
Dealing with finite automaton
Parallel processing
Proof strategies in various contexts
On how real-world systems/problems have been specified using
the Larch approach.
Specs/verification of real world programs, industrial use experiences.
More Larch books [Yikes! Whose going to write all these books?]
================
Integrated with software engineering
Methodology of composing large specifications
Textbooks, case studies
Semantics of LSL
Theoretical fundamentals of LP
Specification and proof strategies for certain
problem domains, e.g. finite automaton, parallel processing
On specific interface languages / case studies / Larch tools
and their usage (maybe like a user-manual?)
Tutorial on algebraic specn. with special reference to Larch.
"Abstraction and Specification in Program Development - Larch Edition."
Tutorial on theorem proving using LP.
Comparison of Larch and other algebraic specification methods.
"Larch in the program life-cycle" or "The Larch program development
methodology." (It depends which you think is primary.)
Mathematical foundations/preliminaries for Larch.
More Larch interface languages for
==================================
VHDL (2 votes)
Oberon
Languages that are more used in specific problem domains, e.g.,
languges used for distributed/concurrent applications,
AI (like Lisp or Prolog), functional programming (like ML)...
More formal semantics of
========================
LSL
LCL
Other
=====
More users!
Pointers to case studies in various contexts, to be published on the WWW
5. What do you perceive to be the advantages and disadvantages of Larch?
a. I like Larch because:
It's simple.
It's a sensible language.
Simplicity and conciseness.
The approach of Larch seems LOGICAL and PRACTICAL (for me).
The 2 tiered approach.
Two tiered nature.
The two tiered approach, with interface specification languages
tailored to the programming language being used. This makes
interface specifications easier to understand for programmers.
Two-tiered approach produces specifications which are easy for
non-logicians to understand, and also useful for static
checking.
The two tiered structure of Larch makes it possible to tie
specifications closely to real programs. It also makes it
possible to build useful light-weight tools.
Procedure specification by means of ``requires, modifies, ensures''
triples giving rise to a simple semantics (hence, making the
languages simpler to understand and reason about for specifiers,
verifiers and implementors).
I find the specification style natural (not surprising!).
It deals with the relation to programming languages in a way
that I think will ultimately be recognized to be necessary
for more widely-used languages, such as Z and VDM.
LSL provides a mechanism for extension with new primitives.
LCLint provides a tool for exploiting partial specifications.
The strong connection to programs
Larch interface languages are closer to software than many existing
specification languages.
Both specification and design are accommodated.
Well targeted to programming languages to allow refinement.
Can be tailored to specific prog. language.
Data type handling.
It is a formal oo language with good tools for supporting
a formal design phase.
I am convinced of the value of the ADT style of program development
(as in "Abstraction and Specification" and as encouraged by CLU.) I
am convinced of the need for rigorous specification of module (i.e.
ADT) interfaces. I find algebraic methods the best fit with this
style of programming. I find 2 level specs provide the best mapping
from specification to code. Although I am not an unqualified devotee
of OOP ( - most of the benefits come from ADTs; thereafter it is not
clear what the balance is between benefits and costs - ) there seems
to be a good fit with algebraic methods. In the presence of
overloading (in the sense of over-riding an implementation) it is
important to be able to say that the over-riding implementation has
the "same" semantics as the over-ridden one. Eiffel has a stab at
this, but is not a sufficiently rich language to do the job properly.
(I guess this could be even more critical in the presence of mutiple
inheritance, but I get a headache thinking about that.)
My principal area of research is in interface specification
languages. I find that the Larch approach to interface specification
is the best of what is currently available. I have been working with
LCL and for the past six months I have been working on a formal
semantics for LCL....
Modularity and genericity of LSL.
The LSL syntax is really cool (using __'s and symbols), wish
I had a macro processor this powerful
Tool support.
It has tool support.
LP is a prover that really works, even for large problems that make
other systems crash. I think you can get used to it quite easily, and
you can get things proved (not quite so easily, though).
I find the Larch Prover a tool that is rather easy to use (once you
have got used to it, of course). I would find it interesting to work
with the rest of Larch, but unfortunately I don't have the time for
this.
[And one person wrote as follows.]
- practically useful research results
- achieved simplicity and usefulness of the proposed languages and tools
- excellent documentation (Larch book, Guide to LP)
- information distribution:
- WWW, larch-interest
- excellent support by Jim Horning and Steve Garland
- excellent tool support (relatively easy to install and use)
b. I don't like Larch because:
Some of the syntax and restrictions in LSL are still quirky. The
languages have not had the polish that comes from hard use. There
isn't an established support community (user's group, newsletters,
university and short courses). I have been unable to persuade my
research colleagues that the cost of support tools is justified
(relative to just writing semi-formal specifications in ad hoc
languages). The up-front commitment and cost seem to be too high for
both product and research groups in my company.
... I do not like algebraic or equational styles of specification.
Although I appreciate the advantages of the Larch approach to
interface specification, this disadvantage has keep me away from Larch
for years.
I prefer to build abstract types from sets, relations etc than
axiomatically.
It is a typed language.
It's based on initial algebras rather than logic.
LSL spec. is too procedural. I prefer more relational expression.
Although I have training in pure maths and mathematical logic (M.Sc.
>20yrs. ago!) and 20 years of software experience, I find it difficult
to understand some of the mathematical details. Maybe many-sorted
algebras weren't taught in my day! I still don't feel confident with
'generated', 'include' etc. In short, I don't feel happy with the
mathematical details; neither do I feel I understand Larch well enough
to know which details I can ignore! (Hence my list of suggested
books/tutorials above.)
I don't understand why an algebraic basis was used. The model based
specifications always seem (to me) more straightforward.
... Unfortunately I don't like the algebraic or equational style of
LSL, hence I have not used LSL or LCL to write non-trivial interface
specifications. I have yet to decide whether I will focus on LCL in
my thesis work on not. (Although I will have to take a final decision
soon!)
Poor user interfaces (but considering problems with portability and
time to be spend for a better user interface (especially for LP), I
regard your omissions as reasonable.
(These complaints may be out of date.)
No support for arbitrary quantifiers, prover lacks decision
procedures, no support for conveniences like lambda-abstraction.
(All this are built into our home-grown Larch and Penelope prover.)
I'm still not convinced that writing formal specifications will
ever become viable in real software development except in
particularily safety critical applications. Hopefully, improved
tool support and effectiveness will change this.
6. Other Information About You
I use these other formal methods, languages, tools:
Z 16
VDM 7
LOTOS 2
CSP 5
TLA 3
Other (1 each)
CCS, HOL, Boyer-Moore, CAMILA (a VDM-like spec. language developed
at Univ. Minho), COQ, VHDL, PVS, Object-Z, home-grown temporal logic, B.
7. Anything else you'd like to add:
If there is anyone else out there who is working on the formal
semantics of LCL or other interface specification languages I would be
interested in getting in touch [Contact: Patrice Chalin, chalin@cs.concordia.ca]
I wrote a paper on the contents of my course, in which we couple Z
for requirements and "refine" the Z document to Larch obtaining a
design document. It is co-authored by P.Ciaccia, and has been
published in the Proc. of the ACM/IEEE Workshop on Sw Engineering
Education, Sorrento 1994. I can send a copy on request. [Contact:
Paolo Ciancarini, cianca@cs.unibo.it]
If you get any comments on improving LCLint, please pass them along to
me. [Contact: David Evans, evs@sds.lcs.mit.edu]
I'm struggling to fit Larch into an overall software development
process. I'm looking at the Cleanroom model at the moment. Has
anyone documented a more-or-less complete formal process from initial
requirements through implementation in which Larch is used?
[Contact: Doug Makofka, makofka@chek.com or makofka@monet.vill.edu]
1. I would like to use Larch on Machintosh+Machintosh CommonLisp/C/C++.
2. Are the source code of LSL,LCL,LP ... published??
[Contact: Shinichi Omura, NCC00310@niftyserve.or.jp]
Is there any plan to have the Larch system run under Microsoft
Windows or Windows NT? Can the system be run on a PC?
[Contact: John J. Rood, jrood@world.std.com]
How about bringing out a volume on Larch that integrates all that
(most of it at least) we know of Larch ? It should have sections for
each Larch language, case studies, Larch tools, and any other
pertinent material. It would be authored by all the people who have
something to contribute to the Larch world. In a line: A one stop
book about Larch !
I missed the Larch tutorial given in Scotland a while back. The South
Coast of England to St. Andrews is (psychologically) about the same
as London to Boston; that is, it requires a days travelling and a
night away at both ends. Besides, we are still very parochial over
here! I don't know how well attended the St. Andrews bash was, but
maybe next time Cambridge, or Oxford, or somewhere in the Midlands,
or even Manchester could be considered. (But please not Central
London - no-one in their right mind goes there by choice these
days :-)
There appear to be very few industrial "stories" about Larch and its
uses. You (as in Jeannette) and a few others (such as Jim Horning)
appear to publish lots of interesting research papers but there appear
to be no experience reports available. This obviously leaves Larch at
a disadvantage compared with VDM, Z, CSP, B, RAISE, ...
References
==========
[Contact Stephen Garland, garland@lcs.mit.edu]
Victor Luchangco, Ekrem Soylemez, Stephen Garland, and Nancy Lynch.
``Verifying timing properties of concurrent algorithms,''
to appear in {\it FORTE'94: Seventh International Conference on Formal
Description Techniques for Distributed Systems and Communications
Protocols}.
J. F. Soegaard-Anderson, S. J. Garland, J. V. Guttag, N. A. Lynch, and
A. Pogosyants, ``Computed-assisted simulation proofs,'' {\it Fourth
Conference on Computer-Aided Verification}, Elounda, Greece, June 1993,
{\it Lecture Notes in Computer Science\/} {\bf 697}, Springer-Verlag,
305--319.
J. Staunstrup, S. J. Garland, and J. V. Guttag, ``Mechanized
verification of circuit descriptions using the Larch Prover,''
{\it Theorem Provers in Circuit Design}, North-Holland IFIP
Transactions A-10, June 1992, 277--299.
J. B. Saxe, S. J. Garland, J. V. Guttag, and J. J. Horning, ``Using
transformations and verification in circuit design,'' {\it
International Workshop on Designing Correct Circuits}, North-Holland
IFIP Transactions A-5, 1992.
[1] [Contact Yang Meng Tan, ymtan@lcs.mit.edu]
@TECHREPORT(TanPhD,
AUTHOR = {Yang Meng Tan},
TITLE = {Formal Specification Techniques for Promoting Software
Modularity, Enhancing Software Documentation, and Testing
Specifications},
INSTITUTION = MITLCS,
YEAR = {1994},
TYPE = {TR},
NUMBER = {619},
MONTH = {June},
NOTE = {PhD Thesis, EECS Dept}
)
Larch Humor
===========
Prize to David Garlan for the funniest answer to Question 2, "Why are
you interested in Larch?"
Well if you must know, I like Larch because of its syntactic virtues.
You see I like to garden and I especially like trees, so naturally
"Larch" is a particularly appealing formal method.
Also, I hate acronyms and short names -- anything under three letters
leaves me cold. So there again Larch wins hand over fist against Z,
VDM, HOL, TLA, B, etc. Of course, it doesn't fare so well with
Boyer-Moore (or even NQthm) by this measure.
Also, I am a rather emotional kind of person, and so when I heard
about Larch's "two teared" model, I was instantly hooked.
Finally, I used to have a friend named Lionel Potter -- but we just
called him LP. So the fact that Larch also involved LP was another
significant factor in my decision to use it.