[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: pvs-help@csl.sri.com*Subject*: Actual arguments in ADTs*From*: "Steven E. Ganz" <sganz@cs.indiana.edu>*Date*: Sun, 15 Jul 2001 18:55:00 -0500*Sender*: pvs-help-owner@csl.sri.com

It seems both safe and useful to allow components of ADTs accepting actual parameters to modify the parameters from those given. As an example, I would like lambda calculus expressions to be typed with a set of potential free variables. Then, judgements about the effects of various syntax-manipulating functions on free variables of an expression can be stated to avoid repetition in proofs. I'd like to write the following ADT, but get an error message that actual parameters are not permitted for locally defined objects. Exp[Ident: TYPE, freeVars: setof[Ident]]: DATATYPE BEGIN ASSUMING identNonempty: ASSUMPTION (EXISTS (i:Ident): TRUE) ENDASSUMING vref(ident: {i:Ident|member(i, freeVars)}): vref? app(rator: Exp, rand: Exp): app? lam(formal: Ident, body: Exp[Ident, union(freeVars, singleton(formal))]): lam? END Exp Is this an enhancement that might be considered, and is there any work-around? Steve Ganz

- Prev by Date:
**Re: commands man pages** - Next by Date:
**Re: Actual arguments in ADTs** - Prev by thread:
**Re: Semantic of IMPORTING** - Next by thread:
**Re: Actual arguments in ADTs** - Index(es):