On Tue, 12 May 2015, Paul Rubin wrote:

> Stefan.Lucks@uni-weimar.de writes:
> You could have a static precondition that accepts proof by assertion,
> like in Coq where you can say "admitted".

Indeed, this is about the thing I am asking for. SPARK 2014 has a pragma 
for that.

>>> Like everyone, I want it all, for free, right now. :-) Only Ada comes
>>> close, and I just want to make it closer.
>> Violent agreement, again!
>
> Do you use other verification systems like Coq?

Tryin out Coq is on my to-do list. Right now, I am only using SPARK 2014 
and the Alt-Ergo prover.

Stefan

------  I  love  the  taste  of  Cryptanalysis  in  the morning!  ------
uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-lucks
--Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany--