• bearophile (93/93) Mar 03 2010 This post is about few other parts of Contract Programming that are not ...

bearophile <bearophileHUGS lycos.com> writes:

This post is about few other parts of Contract Programming that are not present
in D2.

In this page:
http://www.digitalmars.com/d/2.0/dbc.html

This link is dead:
http://pandonia.canberra.edu.au/java/contracts/paper-long.html

You can find that page on the Wayback, I have read this article but I think
it's not very interesting:
http://web.archive.org/web/20040604112142/http://pandonia.canberra.edu.au/java/contracts/paper-long.html

--------------------

old:

Recently I've seen a discussion about "old", but I don't know if it has
produced some conclusion:
http://www.digitalmars.com/d/archives/digitalmars/D/Communicating_between_in_and_out_contracts_98252.html


I've seen that the "old" (regardless its syntax) can be useful to assert that a
function has *not* changed an argument or static/instance attribute:

assert(old.foo == foo);

--------------------

In Eiffel language you can optionally define: loop invariants (that is an
assert) and loop variants (that is an integer expression).

The loop invariant has to be true:
- just after the loop intialization
- after each iteration of the loop body if the loop exit condition is false (so
I think it can be false at the end of the last loop iteration. I don't know why
it's designed like this).

The loop variant is used to be sure the loop terminates after a finite number
of iterations. It's an integer expression that is >= 0 just after the loop
initialization, and it gets decreased by at least one. The loop stops when it
becomes negative.

So far I have never thought about using a loop variant, but there are
algorithms where adding a loop invariant can be useful.

--------------------

This last thing is not present in Eiffel. Maybe it's just an hopeless idea that
can't be implemented in practice.

In an algorithm you can often define an invariant, something that it doesn't
change through it (it can invalidate it in few lines of code that will restore
the invariant soon). Normally in a function you can do it like this:

void foo() {
  // do_something_1
  assert(invariant1);
  // do_something_2
  assert(invariant1);
  foreach (item; items) {
    // do_something_with_item_that_breaks_invariant1_and_restores_it
    assert(invariant1);
  }
  // do_something_3
  assert(invariant1);
}


While you can put asserts in C programs too at the start and end of functions,
contract programming is useful because it allows you to formalize the idea of
precondions, etc, and the compiler can automatically manage class invariants in
presence of inheritance, etc.

Such help from the compiler helps keep the code more tidy, turning normal C
asserts into a something different, a programming paradigm.

So it can be nice to have way that the compiler understands to define an
invariant that's true in a whole block of code. This can be better than putting
many assert(invariant1); scattered into the algorithm, because you have to
write the invariant only once, somewhere at the top of the algorithm, and then
there's no need to sprinkle the code with those asserts. In theory the
compiler/runtime can catch the invariant invalidation sooner and more reliably.

How can the program test the invariant as the code goes run on? In theory the
program has to test the invariant only when a variable that is tested by the
invariant gets written on. But the runtime can do something simpler and more
raw, that is to test the invariant every fixed amount of time (or a bit
randomly in time. There are profilers that are based on random sampling that do
this).

But many algorithms need to break the invariant now and then, so you need a
syntax to disable such invariant tests in a part of the code (like calling
gc.disable(); gc.enable(); for the GC).

Some possible syntaxes (probably all of them are not good):


void foo() {
  invariant1 { // a kind nested function?
    assert(invariant1);
  }
  
  whith invariant1 {
    // do_something_1
    // do_something_2
  }
  foreach (item; items) {
    // do_something_with_item_that_breaks_invariant1
    whith invariant1 {}
  }
  whith invariant1 {  
    // do_something_3
  }
}



void foo() {
  invariant1 { // a kind nested function?
    assert(invariant1);
  }
  
  whith invariant1 {
    // do_something_1
    // do_something_2
    assert(invariant 1);
    foreach (item; items) {
      disable invariant1 {
        // do_something_with_item_that_breaks_invariant1
      }
      assert(invariant 1);
    }
    // do_something_3
    assert(invariant 1);
  }
}



void foo() {
  invariant inv1 { // a kind nested struct?
    assert(invariant 1);
  }

  /// are invariants enabled by default?
  // do_something_1
  // do_something_2
  foreach (item; items) {
    inv1.disable();
    // do_something_with_item_that_breaks_invariant1
    inv1.enable();
  }
  // do_something_3
}

Bye,
bearophile