[Prev][Next][Index]
Draft list of questions for a Larch FAQ list
Hi all,
Below is a draft of a list of questions for a Larch FAQ,
which would eventually make its way to the comp.specification.larch
newsgroup. It has questions, but no answers yet.
Currently we would like to get your comments on
the list of questions. If you don't like some of the ones we have,
or if you have a question you'd like to see added to the list,
please let us know.
Also we're interested in your comments on the copyright notice.
If you think it's too restrictive or have other comments,
please let us know.
Finally, if anyone would like to contribute answers for a question
or a section, we'd be happy to have them. If you'd like to contribute
and maintain a section on an on-going basis, we can add you as a maintainer;
if not, we'll still be happy to acknowledge your contributions.
Gary Leavens (and Matt Markland)
P.S. I know it's final exam time here and elsewhere in academia,
so no rush on this...
Archive-name: larch-faq
Last-Modified: December 6, 1995
Version: 0.7
Maintainers: Gary T. Leavens and Matt Markland <larch-faq@cs.iastate.edu>
----------------------------------------------------------------------
A Frequently Asked Questions list (FAQ) for comp.specification.larch
----------------------------------------------------------------------
This document is intended to be the starting point for generating a
FAQ list for the Larch family of specification languages.
We are looking for more questions to add, and corrections, or additions
to the answers for questions that are posed; please send e-mail
to us at larch-faq@cs.iastate.edu. We welcome and appreciate
any help you may give.
This FAQ is accessible on the WWW in:
http://www.cs.iastate.edu/~leavens/larch-faq.html
A plain text version is also available by anonymous ftp at the URL
ftp://ftp.cs.iastate.edu/pub/larch/larch-faq.txt.gz
Copyright (c) 1995 by Gary T. Leavens and Matt Markland.
Permission is granted for you to make copies of this FAQ
for educational and scholarly purposes, and for commercial use in
specifying software, but the copies may not be sold or otherwise
used for direct commercial advantage; permission is also granted
to make this document available for file transfers from machines
offering unrestricted anonymous file transfer access on the Internet;
these premissions are granted provided that this copyright
and permission notice is preserved on all copies. All other rights reserved.
----------------------------------------------------------------------
TABLE OF CONTENTS
Section 0: Larch and the Larch Family of Languages.
0.1. What is Larch? What is the Larch family of specification languages?
0.2. What is the origin of the name "Larch"?
0.3. How does Larch compare to VDM? Z? COLD? etc.?
0.4. Where can I get more information on Larch and Larch languages?
0.5. Is there an object-oriented extension to Larch?
0.6. What's the use of formal specification and formal methods?
Section 1: The Larch Shared Language. (LSL)
1.0. Where can I get an implementation of LSL and the LSL Checker?
1.1. What's the purpose of a LSL trait? What is a trait used for?
1.2. What are the sections of an LSL trait? What is the purpose of each?
1.3. What's the difference between "includes" and "assumes"?
1.4. How and when should I use a "partioned by" clause?
1.5. How and when should I use a "generated by" clause?
1.6. If an "implies" section is not required, when should I use it?
1.7. How and when should I use a "converts" clause?
1.8. How and when should I use an "exempting" clause?
1.9. Does exempting some term make it undefined?
1.10. How can I exempt only terms that satisfy some condition?
1.11. What's the meaning of a LSL specification?
1.12. Is there support for partial specifications in LSL?
1.13. Can I write assertions using recursion? Does that make sense?
1.14. What pitfalls are there for LSL specifiers?
1.15. Are there any tips for specifying things with LSL you can give me?
1.16. How do I know when my specification is abstract enough?
1.17. Do I have to write all the traits I'm going to use from scratch?
1.18. Where can I find handbooks of LSL traits?
1.19. Where can I find LaTeX or TeX macros for LSL?
1.20. How do I write some of those funny symbols in the Handbook in my trait?
1.21. Is there a literate programming tool for use with LSL?
Section 2: The Larch Prover (LP)
2.0. Where can I get an implementation of LP?
2.1. What is the Larch Prover (LP)? What is LP used for?
2.3. Do I need to use LSL if I use LP?
2.4. Do I need to use LP if I use LSL?
2.5. How do I use LP to check my LSL traits?
2.6. How do I get the LSL checker to generate the files needed by LP?
2.7. What is the use of each kind of file generated by the LSL checker?
2.8. If I run my file through LP and stops, does that mean it's all true?
2.9. What proof techniques does LP attempt automatically?
2.10. What are the basic commands for LP?
2.11. Is there a command reference for LP? Is there a list of LP commands?
2.12. What are most common ways to resume a proof in LP?
2.13. If I made a mistake, how can I backtrack in my proof?
2.14. I'm having trouble proving things like 0 < 2; what am I doing wrong?
2.15. How do I log my proof, and keep track of what has been done?
2.16. Can I save my work so I don't have to reprove things over and over?
2.17. If I include a trait, do I have to reprove everything in that trait?
2.18. Does LP use assertions in the implies section of an included trait?
2.20. What pitfalls are there for LP users?
2.21. Are there any tips on proving things with LP that you can give me?
Section 3: Larch-style Interface Specification Langauges (LISL)
3.0. What is a Larch-style interface specification language (LISL)?
3.1. Where can I get a LISL for my favorite programming language?
3.2. How does a LISL compare to VDM? Z? etc.
3.3. Do I need to write an LSL trait to specify something in a LISL?
3.4. What is an "abstract value"?
3.5. If I specify an ADT using a LISL, do prove it's the same as the trait?
3.6. What does "requires" mean?
3.7. What does "ensures" mean?
3.8. What does "modifies" mean?
3.9. What does "trashes" mean?
3.10. What does "claims" mean?
3.11. What is the meaning of a specification written in a LISL?
3.12. How do I specify that something is finite?
3.13. How do I specify errors or error-checking?
3.14. How do I specify that all the values of a type satisfy some property?
----------------------------------------------------------------------