[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] dependent types in pvs
is it possible to postulate an unknown type valued function in PVS?
When I write something like
types : THEORY
Types : TYPE+
semof : [Types -> TYPE+]
then PVS complains with a syntax error.
My aim is to specify systems that have wires and functional components
and every wire has a type
such as boolean or 32bit-word or whatever and then the semantics of the
system would assign to each time t:posnat and wire w a value of the type
assigned to that wire.
Thanks in advance, Martin