🚀 go-pugleaf

In article <1992Aug25.141510.28180@ibmpa.awdpa.ibm.com> wkh@austin.ibm.com writes:

   Is anyone aware of work on a Larch interface language for SML?
   Seems like it would be a natural thing to do given the SML module
   system.

   Thanks ... WkH
   wkh@dce.austin.ibm.com

   -- 
   Ward K Harold				(512) 838-3473 [T/L 678-3473]
   IBM Personal Systems Programming	external: wkh@dce.austin.ibm.com
   11400 Burnet Rd., Zip 9541		internal: wkh@duke.austin.ibm.com
   Austin, TX  78758			vnet: wharrold --ausvmq


Yes, the Venari Project at Carnegie Mellon University is working on
a preliminary design of Larch/ML, a Larch interface language for ML. 

We've written a paper that describes the initial design and
implementation work. That paper will appear in the proceedings of the
First International Workshop on  Larch, July 13-15, 1992; it is also
available as CMU tech report CMU-CS-92-135 (instructions for FTP'ing
that report are included at the end of this post). 

I've included a brief description of that work here, and would be
happy to answer any other questions. 


Amy Moormann Zaremski
Carnegie Mellon University
Pittsburgh PA 15213
amy+@cs.cmu.edu

=====================================================================

              Larch/ML: A Specification Language for ML
       Gene Rollins, Jeannette Wing, and Amy Moormann Zaremski

The Venari Project is working on a preliminary design of Larch/ML.
The Larch family of specification languages features the Larch Shared
Language (LSL) and interface languages, each tailored to a specific
programming language.  Larch specifications have two components:
traits and interfaces.  LSL traits describe abstractions independent
of any notion of computation state.  A trait looks like a typical
algebraic specification but actually describes more generally a
first-order theory.  Interface language components describe the
behavior of program modules (e.g., ML modules or Ada package),
highlighting their state-changing effects.  Hence an interface
language is defined in terms of the semantics of the target
programming language, specifically its notion of state.

Larch/ML, the Larch interface language for ML, enables one to attach
specification clauses to objects in ML signatures.  A specification
clause for a function consists of a pre-condition, a post-condition,
and a declaration of side effects.  The pre- and post-conditions are
predicates written in terms of LSL trait operators.  One can write
Larch/ML specifications for polymorphic, side-effecting, and
higher-order functions.  Function parameters can be polymorphic and
side-effecting also.  A specification can hence refer to the
specification of a function parameter.  (We have not yet worked out
the full semantics of this feature.)

We are starting to design and implement tools for Larch/ML.  To date
we have a lexical specification, a parsing grammar, and abstract
syntax from which we can generate a syntax checker using sml-yacc and
sml-lex.  We have implemented name scope checking and are currently
implementing type checking.

SML users can embed Larch/ML clauses in SML signatures using special
comments.  They can use an SML compiler to compile Larch/ML sources as
SML signatures; our Larch/ML tools will process the specifications
ignored by the compiler.

As part of the Venari Project, we are planning to use Larch/ML
specifications as search keys for ML program libraries.  The Larch/ML
translator will generate fully-checked abstract syntax trees from
Larch/ML specifications.  We store (in a persistent object base)
abstract syntax trees of module specifications as an index into an ML
program library.  We can then translate specification queries into
checked abstract syntax trees and match them against those in the
index.

=====================================================================

  Instructions for Anonymous FTP of Larch/ML Technical Report:


Ftp to reports.adm.cs.cmu.edu (128.2.218.42) as "anonymous".

At the password prompt, send your Username@site. You must include the
"@" or the login will fail.
  
Then "cd 1992"  

Use the standard ftp commands, such as "get", "cd", "ls", etc.

The reports are in postscript format (.ps).  The index file
is called README.mss.  
The Larch/ML report is CMU-CS-92-135.ps

When you have finished copying the files you need to simply "quit."

=====================================================================