1. Administrative Data People on larch-interest list 66 People responding to survey 45 (68%) Faculty 14 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 12 Formal specification 8 Module interface specification languages 1 Algebraic specs 4 (including equational theories, rewriting) Spec environments 2 Formal verification 5 Hardware 2 Software 4 (compilers, programs, ADTS) Software engineering 10 (design (1), testing (1), prototyping (1), reengineering (1), environments (3)) Programming methodology 5 Distributed 7 (programming, languages and systems) Parallel/concurrent 4 (programming, languages, and systems Languages 10 (design, implementation, semantics) Object-oriented 6 (programming, languages, databases, semantics) Functional 4 (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, applications of logic and algebra to CS. 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 7 Tools (in general) 7 LP (specifically mentioned) 7 Helped develop languages, tools 2 Clarity in Larch documentation 2 Historical 4 Other (1 each) -its semantics -possibilities it offers for static code checking, -good for documenting interfaces -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) 25 LCL (Larch/C Interface Language) 17 LM3 (Larch/Modula-3 Interface Language) 4 Larch/Ada 2 Larch/Smalltalk 2 Larch/C++ 8 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. We're working on documenting part of interviews, but I couldn't say we've done much that would qualify as an extended example otherwise. In general we're interested in Object-oriented stuff... 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 22 LCL checker 11 LCLint 8 LP 28 Penelope 1 Old LSL syntax-directed editor 1 Larch/C++ checker 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 Algebra esp group theory: safety critical case studies using LOTOS. 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 Parameterized sorts and operation names 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@larch.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 Parameterized sorts and operation names Larch/C++ checker ----------------- Type checking, header file generation 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. Tutorial 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)... Unix shell visual BASIC More formal semantics of ======================== LSL LCL Larch/C++ Larch/Smalltalk 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. It allows interface specs to be tailored to a specific programming 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!) LSL suffers compared to OBJ3 in terms of parameterization. There is no good way to specify algebraic constraints or to reuse interface specifications at the level of traits (compared to say the VDM quotation mechanism). 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 3 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@larch.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.