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


Dear pvs users,

I have one problem with the pvs language, and I'll be grateful of your help.

I want to express substitution of a variable X by a term T in another algebraic term. For instance:

    subst(X, T, OP1(X,OP2(Y,Z),Y))

X and T are typed with a previous written datatype. Is there ever exist a theory which allows this feature, or have you got ideas/tracks about that ?

Thank you very much,

Gwen Salaun

Gwen Salaün, PhD Student      Tel: 02 51 12 58 22  Fax: 02 51 12 58 12
IRIN, 2 rue de la Houssinière BP 92208 - 44322 Nantes cedex 3 - FRANCE