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

*To*: pvs@csl.sri.com*Subject*: Enum types as theory parameters?*From*: Pertti Kellomäki <pk@cs.tut.fi>*Date*: Fri, 06 Apr 2001 23:34:07 +0300*Organization*: Tampere University of Technology*Sender*: pvs-owner@csl.sri.com

Is there a way to accomplish something like the following in PVS? th1 [ t : TYPE = {r,s} ] : THEORY BEGIN END th1 th2 : THEORY BEGIN tt : TYPE = {p,q} importing th1[tt] END th2 I.e. I would like to declare that t is an enum type with two values, and I would like to associate p with r and q with s when instantiating th1. The closest I have been able to get is to make t, r, and s all be formal parameters of th1, but then I lose the mutual exclusion property of r and s, and I have to make it an explicit assumption of th1. -- Pertti Kellom\"aki, Tampere Univ. of Technology, Software Systems Lab

**Follow-Ups**:**Re: Enum types as theory parameters?***From:*Dave Stringer-Calvert <dave_sc@csl.sri.com>

- Prev by Date:
**New book: Handbook of Process Algebra** - Next by Date:
**Re: Enum types as theory parameters?** - Prev by thread:
**New book: Handbook of Process Algebra** - Next by thread:
**Re: Enum types as theory parameters?** - Index(es):