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

*To*: Pertti Kellomäki <pk@cs.tut.fi>*Subject*: Re: Enum types as theory parameters?*From*: Dave Stringer-Calvert <dave_sc@csl.sri.com>*Date*: Mon, 09 Apr 2001 13:43:28 -0700*Cc*: pvs@csl.sri.com*In-Reply-To*: Your message of "Fri, 06 Apr 2001 23:34:07 +0300." <3ACE283F.9B99BA16@cs.tut.fi>*Sender*: pvs-owner@csl.sri.com

Pertti - The feature you really want is theory interpretations, a feature of the upcoming PVS 3.0, which would allow you to provide an enumeration type in th1, another in th2, and provide a mapping between them. E.g. % % PVS 3.0 % th1 : THEORY BEGIN t : TYPE = {r,s} END th1 th2 : THEORY BEGIN tt : TYPE = {p,q} IMPORTING th1{{r:=p, s:=q}} END th2 In the current version of PVS, you can get close to what you need by using an assumption on the formal parameter of th1. This gives you the property that the instantiating theory must use a two valued type - if you need other properties, e.g. the induction principle, you could add those into the assumptions as well. % % PVS 2.3 % th1 [t : TYPE+] : THEORY BEGIN ASSUMING two_disjoint_values_for_t : ASSUMPTION EXISTS (a,b : t) : a /= b AND FORALL (value : t) : value = a OR value = b ENDASSUMING END th1 th2 : THEORY BEGIN tt : TYPE = {p,q} IMPORTING th1[tt] END th2 Hope that helps, Dave --- Dr Dave Stringer-Calvert, Senior Project Manager, Computer Science Lab SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA Phone: (650) 859-3291 Fax: (650) 859-2844 David.Stringer-Calvert@sri.com

**References**:**Enum types as theory parameters?***From:*Pertti Kellomäki <pk@cs.tut.fi>

- Prev by Date:
**Enum types as theory parameters?** - Next by Date:
**Re: Predicate subtypes** - Prev by thread:
**Enum types as theory parameters?** - Next by thread:
**Re: Predicate subtypes** - Index(es):