I'm writing a DbC (Design by Contract) library for Nim and I would like you to
give me your thoughts on this topic (references at the end).
I wanted to get into Nim's code transformations so I thought it would be a good
idea to try implementing some simple libraries. Actually, this one was ready in
the present form more than two months ago but I didn't feel like publishing it
yet as it lacked crucial (or so I thought) features like, let's say,
inheritance. Due to lack of time (and being lazy).
# Compiler extensions / module-range macros
As far as I know, Nim deserves a name of "extremely statically compiled
language", one of the reasons being advanced compile-time checks (like
overloading for _static_ arguments or _noSideEffect_ pragma). It sounds
reasonable to extend it with a prover. I thought it would be nice to use it
just like any other nimble package. Unluckily just importing a package can't
(as far as I know) enable any code transformation for the module (unlike Rust
plugins) but wrapping the code doesn't sound all that bad. Maybe anyone here
have better ideas for making an easy-to-install compiler extension?
# Exceptions
I'm not sure if exception-aware contracts would be a good thing to do. Of
course they would complicate proving process but if any exception possible to
throw would need to be included in contract signature so that the prover knows
what conditions are fulfilled if the exception is raised (or even why it could
be thrown), it could probably help using formal contracts in error-prone
environments.
Why even bother? There are cases when we can't guarantee that the operation
will be finished successfully but we can, let's say, promise that even if it
doesn't, it won't corrupt it's arguments. Like impossible swap will just leave
it's arguments as they are.
# Type invariant inheritance
I have seen at least three approaches to type invariant (single) inheritance
none of which sounds perfect. Some reasonable contracts are difficult to write
down using variable-oriented type invariants but using quantifiers, while
handy, is troublesome in implementation if it's bound not to be ridiculously
inefficient.
It seems to me that UML-like contracts could be a good idea but... they only
handle very specific traits (e.g. _add-only_, _unique_, _sorted-by_). It could
be also nice to introduce analogical traits for subroutines, e.g. _commutative_
or _associativeWith_. Maybe custom contractual traits declarations would do?
What grammar should contractual type invariants (or type traits) use? Nim's
grammar seems a bit limited here (especially lack of macro-pragma for fields)
and macros have to accept parsable Nim. I considered a few possibilities:
* mock field – objects-only; as the contract's body is parsed as the field's
type, no more than one expression is accepted
type parityPair = object of RootObj
a: int
b: int
invariant:
a + b mod 2 == 0
* invariant subroutine – less compact, doesn't seem like a part of the
language; using the type before declaring invariant possible
invariant(p: parityPair) =
p.a + p.b mod 2 == 0
anotherRule(p.a, p.b)
* new type declaration block – seems less natural
typeWithInvariant parityPair of RootObj:
a: int
b: int
invariant:
a+b mod 2 == 0
anotherRule(a, b)
Of course there are other details like how to express 'previous iteration'
concept gracefully and many more.
Glad for any help.
Basics:
[https://en.wikipedia.org/wiki/Design_by_contract](https://en.wikipedia.org/wiki/Design_by_contract)
My library on github:
[https://github.com/Udiknedormin/NimContracts](https://github.com/Udiknedormin/NimContracts)
