[SystemSafety] C for OSs

[David Crocker]

We implemented something similar (i.e. template instantiation
preconditions) in Perfect Developer back in 2002. I don't remember any
particular issues with the theorem prover, however the generics we
supported were parameterized only on types, not on integers.

Unfortunately, C++ makes it necessary in the general case to verify
every instantiation of a template separately, rather than verifying the
template only once, unless some stringent conditions are met e.g. no
template specialisation is used.

David Crocker, Escher Technologies Ltd.
http://www.eschertech.com
Tel. +44 (0)20 8144 3265 or +44 (0)7977 211486

On 16/09/2019 11:13, Roderick Chapman wrote:
> 1. In late 2012 (when I first read it), it quickly became apparent
> that there was _no_ tool support at all for this "Concepts" based
> generic programming.  We designed something similar in SPARK2005 back
> in the day (it never got finished unfortunately), and it requires a
> theorem-prover of some sophistication to verify that generic
> instantiations really are OK.