3 ms·
It wouldn't surprise me if even Frama-C and SPARK have a "trust me" annotation.
by solidsnack9000 9y ago
It wouldn't surprise me if even Frama-C and SPARK have a "trust me" annotation.
- nickpsecurity 9y agoPretty much all languages w/ formal specifications do. The reason is that some specification claims are assumed/reasonable, proven outside the tool, or too hard to handle immediately. This can also be used as a maybe later. I'm not sure what theirs are.