The Semantics of C++ Data Types: Towards Verifying low-level System Components
Michael Hohmuth, Hendrik Tews · 2003
Data[Semantics int] dt int exists : Axiom Exists (x: (pod data type?[Semantics int])): True dt int : (pod data type?[Semantics int]) End Cxx Int The identifiers with sshort refer to the corresponding items from the semantics of signed short. First we declare the size of the value representation, this becomes important for the unsigned integer types, see below. We define the value type Semantics int as a predicate subtype of the PVS integer type int. The axioms int longer and int contains sshort formalise the requirement that "[short int] provides at least as much storage as [int]" (3.9.1 (2)).