Hacker News Reader

Comment by klibertp | Hacker News Reader

See the papers "Soft Contract Verification" and "Soft Contract Verification for Higher-Order Stateful Programs" (Nguyễn et al.) In general, there's a lot of academic work on the topic coming from the Racket community.

In short: yes, some classes of contracts can be statically proven. Not all of them, and it depends on the language's semantics, so it's probably not easy to retrofit into C++. But there's work being done on unifying types and contracts, moving back and forth between static proof and dynamic enforcement, and it's all pretty interesting. Proving contracts statically eliminates runtime overhead; generating contracts from types makes it possible for a gradually typed language to be sound.

View on HN

"Verified Design-By-Contract" has been implemented for C/C++ (annotated subset) by David Crocker in his Escher C/C++ Verifier - https://www.eschertech.com/products/ecv.php and https://www.eschertech.com/products/verified_dbc.php

More links in my previous comment chain here - https://news.ycombinator.com/item?id=48544022

The basic idea is that you generate "Verification Conditions"(VCs) by mapping the function onto a Hoare Triple viz. {Pre} Function-Body {Post} and then applying Dijkstra's WP-Calculus mechanically to step backward from the Post to the Pre thus generating a mathematical formula.

The programmer provided contracts are merged into this formula to generate the complete VC which is a logical implication viz; Pre ==> WP(contracts-from-function-body, Post).

This is then handed off to a automated solver which verifies that Post is met when Pre is True in all the paths.

See also, Combining Tests and Proofs with Contracts for Better Software Verification - https://news.ycombinator.com/item?id=50108206

I haven't seen those papers. The general thought seems to be that progress is good enough that a restricted subset of C++ can be proved (which is getting less restricted all the time, though probably never will be everything) and the solvers will be able to detect where they give up: if you want a solver you will have to write the code they can prove and that is an acceptable limitation.

Contracts also allow a solver to say "I can't prove this messy function, but I can at least prove everything around it". Which is to say if we prove the precondition is met, and if we assume the post conditions are met, we can prove everything else despite the messy parts we can't do. This at least lets us know where the messy code is.

https://news.ycombinator.com/item?id=50108112

Reply on news.ycombinator.com