[HN Gopher] Adding "invariant" clauses to C++ via GCC plugin to ...
___________________________________________________________________
 
Adding "invariant" clauses to C++ via GCC plugin to enable Design-
by-Contract
 
Author : gavinray
Score  : 23 points
Date   : 2023-01-01 22:02 UTC (58 minutes ago)
 
web link (gavinray97.github.io)
w3m dump (gavinray97.github.io)
 
| MuffinFlavored wrote:
| The B-Tree invariant example in the unit test seems like a bunch
| of assertions. Feels very similar to unit tests? Am I missing
| something?
| 
| Assert at runtime or assert at unit test time, it's assertions
| all the way down? Not sure the benefit of some weird @decortator-
| like syntax to achieve 5-10 lines of assertions?
 
  | vlovich123 wrote:
  | Very similar but I suspect most people don't use asserts
  | properly so this is more of an opinionated approach that makes
  | it more difficult to misuse.
 
| kgeist wrote:
| What's the advantage of invariants over unit testing? Seems like
| there must be lot of overhead at runtime.
| 
| >I was ending up with garbage, and not realizing it until I had
| visualized it with Graphviz!
| 
| >Imagine if we had invariants that we could assert after every
| property change to the tree.
| 
| Have you tried writing unit tests? What didn't work about them
| that you decided to try invariants?
 
  | charcircuit wrote:
  | This isn't a replacement for unit tests. This is an alternate
  | syntax to using asserts. You would still want unit tests to see
  | if those asserts are being violated.
 
  | Someone wrote:
  | Not the writer, but it seems obvious to me. It's a luxury
  | version of _assert_. You leave them enabled in debug builds to
  | get better bug reports from testers.
  | 
  | Those testers may hit cases you forgot to write unit tests for.
  | 
  | Of course, you can also forget to write invariants, or write
  | invariants that are less tight than they should be, but I think
  | it often is easier to write invariants than to write exhaustive
  | unit tests.
  | 
  | Firstly, writing " _p_ should always be a prime" is clearer
  | than writing "if _p_ is a prime, and you call _f_ , _p_ should
  | be a prime afterwards", and secondly, invariants can apply to
  | multiple methods that you, otherwise, would have to write
  | separate tests for (" _foo_ keeps _p_ a prime", " _bar_ keeps
  | _p_ a prime", " _bar_ keeps _p_ a prime when called with a null
  | argument", " _baz_ keeps _p_ a prime if it throws an
  | exception", etc)
  | 
  | Also, invariants, IMO, can be way better documentation than
  | unit tests.
  | 
  | Finally, invariants leave open the possibility of using a
  | theorem prover to (dis)prove that they hold.
 
  | pstrateman wrote:
  | It's more likely that they'll get updated correctly when the
  | surrounding code is changed.
  | 
  | Unit testing requires someone to enforce they get updated.
 
  | balfebs wrote:
  | The post assertions do look very similar to a unit test, but
  | the pre assertions seem really useful; it can sometimes be
  | difficult to know every code path that leads to your function,
  | and though tools exist for this, assertions on inputs help you
  | catch errors arising from unusual conditions.
  | 
  | This seems like it's mostly syntactic sugar for assertions,
  | keeping them at the interfaces of the function (in and out).
  | 
  | It can also be sometimes useful to have these conditions right
  | there alongside the implementation and not just somewhere else
  | in your unit tests.
 
  | westurner wrote:
  | icontract is one implementation of Design by Contract for
  | Python; which is also like Eiffel, which is considered ~the
  | origin of DbC. icontract is fancier than compile-time macros
  | can be. In addition to Invariant checking at runtime, icontract
  | supports inheritance-aware runtime preconditions and
  | postconditions to for example check types and value
  | constraints.
  | https://icontract.readthedocs.io/en/latest/usage.html#invari...
  | 
  | For unit testing, there's icontract-hypothesis; with the
  | Preconditions and Postconditions delineated by e.g. decorators,
  | it's possible to generate many of the fuzz tests from the
  | additional Design by Contract structure of the source.
  | 
  | From https://github.com/mristin/icontract-hypothesis :
  | 
  | > _icontract-hypothesis combines design-by-contract with
  | automatic testing._
  | 
  | > _It is an integration between icontract library for design-
  | by-contract and Hypothesis library for property-based testing._
  | 
  | > _The result is a powerful combination that allows you to
  | automatically test your code._ Instead of writing manually the
  | Hypothesis search strategies for a function, _icontract-
  | hypothesis infers them based on the function's [sic]
  | precondition_
 
  | nimish wrote:
  | They are declarative vs imperative and sufficiently smart
  | tooling exists such that they can be checked and enforced
  | statically, see liquid haskell and "refinement" typing for an
  | example. Formal verification starts to become a possibility --
  | enforcing both conformance and documentation.
  | 
  | Tests are fine too but more tedious work.
 
___________________________________________________________________
(page generated 2023-01-01 23:00 UTC)