Re: [PVS-HELP] Datatype subtype problem

[Sam Owre <owre@xxxxxxxxxxx>]

Hi,

Could you tell me which version of PVS you're using?  When I tried this
spec, I got the error "Name Vars already in use as a type".  This is
correct, as the Vars type in the Expr parameters list may not be used as a
subtype in rhs.

Sam Owre

fsong <fsong@sei.ecnu.edu.cn> wrote:

> Dear Everyone:
> 
> I define a theory which contain a Datatype like is:
> 
> Expr [Vars,Value: TYPE+]: THEORY
> BEGIN
>   IMPORTING env[Vars,Value]
>   Expr_terms:  TYPE=[Env->Value]
>   Bexpr_terms: TYPE=[Env->bool]
>  
>   rhs :DATATYPE WITH SUBTYPES Vars,Expr_terms,Value
>   BEGIN
>     expression(e: Expr_terms)      :expr?          : Expr_terms
>     variable(v: Vars)              :va?            : Vars
>     constant(v: Value)             :con?           : Value
>   END rhs
> END Expr
> 
> Then I want to declare
>   x,y   :Vars
>   v1    :[Vars,rhs] =(x,y)
> it is error in y, the type is not match . But I have declared "Vars" is subtype
> of rhs.
> 
> Is anyone know what`s wrong.