Y
HN Search
Hacker News Search
new
|
comments
|
top
|
jobs
xentropy
searching PlanetScale…
1.
▲
2.
▲
3.
▲
4.
▲
5.
▲
6.
▲
3 ms
·
1.
▲
by
xentropy
6y ago
I don't know details. GNATprove generates verification conditions (conjectures) from SPARK code and assertations. Then it feeds these verification conditions to proof tool (Why3, Alt-Ergo, CVC4 or Z3). https://github.com
2.
▲
by
xentropy
6y ago
Runtime checks are compiler implementation issue rather than language issue itself. With static analysis compiler could eliminate redundant runtime checks. For example, if SPARK (Ada subset) is used and absense of runtime errors can be prov