On Thursday, 5 February 2015 at 09:43:53 UTC, Jonathan M Davis
wrote:
There is no such difference in the current implementation.
assertions inside
of in and out blocks are no different from assertions inside of
the
functions themselves with regards to when they are compiled in
or not.
But that is a compiler issue, and not a general issue with
interface contracts for components.
What is desirable is to have "asserts with semantics attached to
them" done in a way that works with how you do formal program
verification. I also would like to see loop invariants getting a
special treatment.
pass. Regardless,
if you have
auto foo(T t)
in
{
assert(something about t);
}
body
{
...
}
it's _identical_ to
auto foo(T t)
{
assert(something about t);
...
}
Yes and just having an alias "precondition" for "assert" would go
a long way in that case. And if the compiler recognize it, it
could also do the magic for inheritance.
with regards to semantics. Ideally, what's in the in block
would be compiled
in if the caller is compiled with assertions enabled with no
regard to
whether the library with foo in it was compiled with assertions
enabled or
not, but that's not how it works. And because D allows for
function
prototypes where the implementation is hidden, it's not at all
obvious how
it would even be possible for anything in an in our out block
could be
compiled in or not based on the caller rather than the function
itself.
I actually think that interface contracts (and ideally unit
tests) should be part of a specification language that is shared
across implementation languages. Then the implementation language
has to provide mechanisms to make it possible to test that the
transitions between components abide interface contracts.
The ideal build system would allow you to have one specification
with pre/post conditions between modules and then let the build
system link together "LLVM IRish object code" with checks between
modules injected duing whole program optimized "linking".
That way you could build large systems that are more robust using
code from C, C++, Ada, Fortran, Rust, D... governed by one
unified specification. And a combination of proof verification
and an optimizing linker could elide pre/post-condition tests
that are redundant, either before a formal proof exists that only
needs to be verified or because the condition is trivially
satisifie, e.g.:
----
func(int i){
precondition(i>0);
...
}
----
func(3);
-----
