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

Subtyping



I try to express in PVS that the unnamed function (Lambda (x:P) :
expression) has a result of type Q.
I don't find a solution (without giving a name) through the reference's
manual.

Motivation :
in Hoare Logic the expression {P}M{Q} means that the program M starting
in a state satisfying P, terminates in a state 
satisfying Q.
I want to give a functional translation f(M) of M, and to verify in PVS
that f(M) : [P -> Q], this fonctional translation is done by recurrence
on M and is a lambda-expression without name.
I try to reproduce in PVS a study already done in COQ by J.C.Filliatre.

	Sincerely yours
-- 
Michel Levy  
D106 - L.S.R.     
B.P.72 - 38042 SAINT MARTIN D'HERES CEDEX - France
e.mail : Michel.Levy@imag.fr    tel :(33)476827246
http://www-lsr.imag.fr/Les.Personnes/Michel.Levy