[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.
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==============================

People on larch-interest list				66
People responding to survey				43 (65%)

Faculty						12
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
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/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

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

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.

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):

software engineering					 3
formal methods (including just one lecture)		 4
programming with Modula-3				 1

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
==================================

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
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

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

(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.

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

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.