Other parts of Contract Programming

[bearophile]

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