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

function that returns the element of a singleton passed to it as aparameter.



Dear PVS Gurus:

I'm trying to do something perhaps unusual with PVS. I am trying to define a
function called breaker() that returns the element inside a singleton passed to
it as a parameter. I have a function called builder() that takes a scalar (like
a nat) and turns it into a singleton. So, breaker( builder( x ) ) = x .

The definition of builder( a:elem ) : setof[elem] = { (x:elem) | x = a }.

Would you have any suggestions as to how one might define breaker()? I'm a PVS
novice, and have tried everything a novice might. Of course, I've been trying
to use the axiom I mentioned above in my proofs, but ultimately it fails to
serve my purpose.

If you're curious, I am trying to formalize something called Bunch Theory, a
theory of sets (sort of, anyway) by Eric Hehner (U of Toronto), which I can
then use to prove the correctness of object-oriented systems using
refinement. 

Warmest regards,

Andrei Rotenstein
-------------------------------------------------------------------------------
Eternal Student, Department of Computer Science, York University
http://www.cs.yorku.ca/~andrei
-------------------------------------------------------------------------------

   Bathquake, n.: The violent quake that rattles the entire house when
   the water faucet is turned on to a certain point. -- Rich Hall,
   "Sniglets"