[Prev][Next][Index]

Re: Higher-order operators

Jeannette et al,
	You might also mention that LM3 has some provisions for handling
procedure parameters.  It can talk about the specification of the procedure
parameter, and about intermediate states.  However, it doesn't seem to
be fully general in the execution seqences it can discuss.

In this vein it may be worthwhile to mention the following papers.
The first gives a sound and relatively complete Hoare-logic for reasoning
about procedure parameters.  

@Article{Ernst-Navlakha-Ogden82,
  Key = 	"Ernst \& Navlakha \& Ogden",
  Author = 	"George W. Ernst and J. K. Navlakha and W. F. Ogden",
  Title = 	"Verification of Programs with Procedure-Type Parameters",
  Journal = 	"Acta Informatica",
  Year = 	1982,
  Volume = 	18,
  Number = 	2,
  Month = 	Nov,
  Pages = 	"149-169"
}

This next paper is similar to the previous one, but handles generics as well.

@Article{Ernst-etal91,
  Key = 	"Ernst, {\em et al.}",
  Author = 	"G. W. Ernst and R. J. Hookway and J. A. Menegay and
		 W. F. Ofgen",
  Title = 	"Modular Verification of {Ada} Generics",
  Journal = 	"Computer Languages",
  Year = 	1991,
  Volume = 	16,
  Number = 	"3/4",
  Pages = 	"259-280"
}

The following uses higher-order logics to do verification.
I'm sure it's appeared already, but I don't have the up-to-date citation.

@TechReport{German-Clarke-Halpern88, Key="German \& Clarke \& Halpern",
Author="Steven M. German and Edmund M. Clarke and Joseph Y. Halpern",
Title="Reasoning about Procedures as Parameters in the Language L4",
Institution="GTE Laboratories, Inc.",
Address="Waltham, Mass.",
Month=Oct,
Year=1988,
Note="To appear in {\em Information and Computation}",
Annote="25 references."
}

My question would be why don't one of these approaches work in the
context of a Larch-style interface specification language?
Perhaps they need to be combined with the reification of state
as in LM3?  Perhaps people don't want to deal with a specification
that is essentially a denotational semantics (as would result from
using explicit states), or with higher-order logic?

	Gary
Reference(s):