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

Re: Enum types as theory parameters?




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