31 ms·
Are that static or runtime checks (or both)?
by still_grokking 5y ago
Are that static or runtime checks (or both)?
- Jtsummers 5y agoDefinitely runtime, potential for compile time. The compile time checks will at least prevent obvious cases (assigning a value out of the range like using either Byte type above: T := -1 will get a compile time error). Using the second Byte type, paired with SPARK/Ada, this bit of code should set off the proof system and prevent compilation: procedure Foo is type Byte is range 0..7; T : Byte := 0; begin T := Byte - 1; end Foo; (Not that that's useful code, but a basic example.) That shouldn't make it past the SPARK/Ada system to compilation. Now change it to this: function Foo(T : Byte) return Byte is begin return T + 1; end Foo; and SPARK/Ada should warn (been a bit, but should also fail to compile) that this could cause overflow.