Weblogs Forum
Can Contracts be Equated with Types?

38 replies on 3 pages. Most recent reply: Aug 18, 2006 3:45 AM by Achilleas Margaritis

 Previous Topic Next Topic
 Flat View: This topic has 38 replies on 3 pages [ « | 1 2 3 | » ]
 Vladimir Nesov Posts: 27 Nickname: robotact Registered: Aug, 2005
Re: Can Contracts be Equated with Types? Posted: Aug 10, 2006 2:33 AM
> Anyway, for anyone interested, the idea is:
>
> A block of code has a set of inputs (allowed values) and
> outputs (possible outcomes). When two blocks of code are
> paired up in a sequence, the outputs of the 1st block must
> be a subset of the inputs of the 2nd block. A compiler
> rejects a block of code that does not conform to this
> simple rule. This technique could enable static contract
> evaluation.

How can such input and output be defined/determined? There should be powerful abstraction on what input/output is to make such thing robust. Anyway it's basically what all static analyzers are trying to do, and all ruminations are around what is appropriate approximation of input/output (data flow).

Or is the point is that one doesn't need to determine data flow to check this property? But for procedure calls one needs to compare effects of called procedures, and it seems to require some sort of data flow.

 Achilleas Margaritis Posts: 674 Nickname: achilleas Registered: Feb, 2005
Re: Can Contracts be Equated with Types? Posted: Aug 10, 2006 5:48 AM
> This sounds interesting. Do you have any ideas about
> recursion?
>
> For example:
>
> f = a b [f] if
>
> How do you make sure that the output of f is correct if it
> depends on f itself (and maybe on the correctness of f)?

Let's see the factorial function (written analytically). The contract is that the input is greater than 0:

`1    int fact(int n : n >= 0) {2        int result;34        if (n == 0) {5            result = 1;6        }7        else {8            int n1 = n - 1;9            int f = fact(n1);10           result = n * f;11       }12       return result; 13   }`

Here is the analysis:

`Line Input                   Output           ------------------------------------------1    n(int)                  n(0 | pos int)   4    n(0 | pos int)          n(0)5    n(0)                    result(1)8    n(pos int)              n1(0..n-1)9    n1(0..n-1)              f(pos int)10   n(pos int), f(pos int)  result(pos int)12   result(1, pos int)      result(pos int)`

Explanation:

line 1 : the input number must be greater than or equal to zero. Therefore, for the rest of the block, it is considered so.

line 4 : the static if n == 0 makes sure n is 0 inside the then block.

line 5 : the result is 1.

line 8 : since line 4 is executed only if n == 0, it means n is a positive integer, not zero, for lines 8-10. Therefore, n1 is >= 0 due to the subtraction with 1.

line 9 : n1 is a legal value for passing it to 'fact', because n1 >= 0. Since n1 is a subset of n, the end result is 1 (already computed), so f can only be a positive number.

line 10 : the result of the multiplication is a positive integer, since both n and f are >= 1.

line 12 : the result is either 1 or a positive integer i.e. the result is >= 1.

I am sure there are some holes in the above, I am no mathematician...but I guess whatever abstraction can I do with my brain, I can pass it to the computer, provided that it is formed correctly.

 Vladimir Nesov Posts: 27 Nickname: robotact Registered: Aug, 2005
Re: Can Contracts be Equated with Types? Posted: Aug 10, 2006 6:39 AM
Problem is that if constraint is any complex, you'd need to force it at least local inside the method, analyser wouldn't be able to check that forced annotation is indeed correct. Though creating practical solution on at least this level would be great by itself.

 Jules Jacobs Posts: 119 Nickname: jules2 Registered: Mar, 2006
Re: Can Contracts be Equated with Types? Posted: Aug 10, 2006 8:12 AM
> line 9 : n1 is a legal value for passing it to 'fact',
> because n1 >= 0. Since n1 is a subset of n, the end result
> is 1 (already computed), so f can only be a positive
> number.

Do you have any ideas about the implementation of this, specifically this:

"the end result is 1 (already computed), so f can only be a positive number."

I have no idea how to implement this reasoning in a computer program. The compiler has to prove that for every call to fact the end result will be 1. So if you subtract 1 from n you'll reach the base case eventually.

Do you think it's possible to prove this in more complex cases? To me this sounds like the halting problem...

 Vladimir Nesov Posts: 27 Nickname: robotact Registered: Aug, 2005
Re: Can Contracts be Equated with Types? Posted: Aug 10, 2006 10:32 AM
This particular problem can be estimated well, you'd need to apply "widening" in loop junction points, in this case recursion creates a loop. After several iterations (result of first is that return value of fact() is 1, result of second is that it's in interval [1,2], etc.) one can extrapolate changes, extending initial value 1 in direction of change, obtaining [1,+inf) in result. Few iterations after that are likely to impose possible upper constraints.

Problems begin from simpliest C construction such as `char buf[1000];...for(int i=0;buf[i]!=0;++i) ...`It can be handled using some heuristics, but it's just an example, custom construction will create such obstacles again and again. One can create for_each function which by its contract guarantees that collection is traversed correctly, but such assumbtion will need to be expressed explicitly without checker being able to check if it's really so for some complex combination of custom container implementation and access to the same container within the loop.

Another problem is ubiquitous aliases. Alias analysis problem is yet to be solved, and propagation of annotations associated with values seems to inevitably require alias information.

 Eelis van der Weegen Posts: 2 Nickname: eelis Registered: Aug, 2006
Re: Can Contracts be Equated with Types? Posted: Aug 10, 2006 11:28 AM
I'd like to make two points:

First, it's possible to reason about the input/output correctness of algorithms, at least in systems that were designed for this purpose. To illustrate this point, I will prove the >0 output guarantee of the factorial function in one such system, namely Coq (the same one I mentioned before).

First, we define factorial in a straightforward way:
`  Fixpoint fact (n: nat): nat :=    match n with    | 0 => 1    | S m => (fact m) * n    end.`

(nat is the type of natural numbers.)
Next, we formally prove the >0 guarantee in an accompanying lemma:
`  Lemma fact_result: forall n, (fact n) > 0.    unfold gt.    induction n.      simpl.      apply lt_n_Sn.    simpl.    replace 0 with (0 * fact n).      replace (fact n * S n) with (S n * fact n).        apply mult_lt_compat_r.          apply lt_O_Sn.        assumption.      rewrite mult_comm.      reflexivity.    reflexivity.  Qed.  `

The proof is pretty unreadable in this form unless one has experience proving things in Coq, but the essence is just proof by induction on n.

The second point I'd like to make is that if the type system is expressive enough, these input/output guarantees can be expressed as types (rather than as accompanying lemma's), exactly like the opening poster theorized.

In Coq, functions whose input/output types incorporate pre- and postconditions are called strongly specified, as opposed to weakly specified functions whose input/output types do not. The fact definition above is an example of a weakly specified function. To illustrate the difference, here's a strongly specified version of fact:
`  Lemma one_gt_zero: 1 > 0.    unfold gt.    apply lt_n_Sn.  Qed.    Lemma rec_call_valid (rec_val n: nat) (rec_spec: rec_val > 0): (rec_val * S n) > 0.    unfold gt.    intros.    rewrite mult_comm.    replace 0 with (0 * rec_val).      apply mult_lt_compat_r.        apply lt_O_Sn.      assumption.    reflexivity.  Qed.    Fixpoint fact_strong (n: nat): { r: nat | r > 0 } :=    match n with    | 0 => exist _ 1 one_gt_zero    | S m => let (rec_val, rec_spec) := (fact_strong m) in        exist _ (rec_val * (S n)) (rec_call_valid _ _ rec_spec)    end.`

The details of what's going on here are unfortunately more complex and involve some Coq specifics, so I won't go into them. The key point however is that the return type has changed from plain nat to { r: nat | r > 0 }, which is a pair-like (and dependent) type consisting of a nat and a proof that said nat is greater than 0. The definition of fact_strong uses the two smaller lemmas (which are now merely implementation details) to produce the result value and the >0 proof simultaneously.

These examples really only show the tip of the iceberg of what's possible. The research field that studies the various interesting relations between type systems, logic, proofs, algorithms, and correctness, is called Type Theory. Before I was introduced to Type Theory, I pretty much had the same gut-feeling as the opening poster about the potential of type systems, and learning about Type Theory was an incredible eye-opener for me.

Unfortunately, all of the above is currently somewhat acedemic; the type systems and formality of semantics of conventional/mainstream programming languages are not nearly expressive or "pure" enough to be able to effectively express let alone prove nontrivial properties of programs written in them.

That said, most programmers probably can't be bothered with all this proving business anyway, although that may be somewhat of a defeatist attitude ;-).

 Vladimir Nesov Posts: 27 Nickname: robotact Registered: Aug, 2005
Re: Can Contracts be Equated with Types? Posted: Aug 10, 2006 12:02 PM
Eelis van der Weegen
I'll look into this field.
How do you assess proof expenses, that is time required to develop proved code (at least properties which guarantee no buffer overflows, resource leaks, etc. common stuff) vs. time to develop unproved code (maybe with tests) for some usual code portion which is a part of not-small system?

 Andrei Korostelev Posts: 5 Nickname: andreika Registered: Aug, 2006
Re: Can Contracts be Equated with Types? Posted: Aug 12, 2006 4:42 AM
Contracts have semantic nature, i.e. bahavior.
Types have syntactic nature.

It is clear that possibilities to express behavior only in terms of traditional type compatibility are very limited.

The question whether the type system need to support behaviour compatilbility depends on the abstraction level.

For example SOA-based systems rely on behavior compatibility between services, whereas C++ language(as an example) used to implement these services relies on a static type system to provide maximum performance.

 Jules Jacobs Posts: 119 Nickname: jules2 Registered: Mar, 2006
Re: Can Contracts be Equated with Types? Posted: Aug 12, 2006 4:48 AM
Types also have a semantic nature. Overloading for example, is built on top of types.

 Andrei Korostelev Posts: 5 Nickname: andreika Registered: Aug, 2006
Re: Can Contracts be Equated with Types? Posted: Aug 12, 2006 1:37 PM
Overloading has compile-time resolution, whereas bindings built on top of contracts are resolved at run-time.

 Jules Jacobs Posts: 119 Nickname: jules2 Registered: Mar, 2006
Re: Can Contracts be Equated with Types? Posted: Aug 13, 2006 3:00 AM
True, but what is your point?

Syntax = semantics.

You can have contracts in a turing complete language that doesn't support them natively. They just have a different syntax.

 Andrei Korostelev Posts: 5 Nickname: andreika Registered: Aug, 2006
Re: Can Contracts be Equated with Types? Posted: Aug 13, 2006 10:22 AM
My point is that modelling behavior in terms of traditional type compatibility is often not enough to catch runtime semantics of component/service contracts.

Here I to refer the idea expressed by Rockford Lhotka in his "A SOA Versioning CovenantA SOA Versioning CovenantA SOA Versioning Covenant" article, http://www.theserverside.net/tt/articles/showarticle.tss?id=SOAVersioningCovenant

In this article he made a distinction between semantic contracts, which is "the definition of an API or a message schema in terms of data types and method signatures" and semantics contracts, which indeed model behavior. The idea was that building systems basing on services semantic contracts, as opposite to syntactic conmtracts, increases flexibility of such systems.

 Andrei Korostelev Posts: 5 Nickname: andreika Registered: Aug, 2006
Re: Can Contracts be Equated with Types? Posted: Aug 14, 2006 12:42 AM
Correction for the last paragraph:
...distinction between syntactic contracts and semantic contracts

 Max Lybbert Posts: 314 Nickname: mlybbert Registered: Apr, 2005
Wonderful Posted: Aug 15, 2006 8:30 AM
I honestly thought things had petered out here, so I was sad my wisdom would be missed (g). So I'm glad people have kept the flame alive.

One of the fundamental bits of advice I got from The C++ Programming Language is that "classes should have a clear invariant." By feeding data to a class, you get objects. The class should make sure, at all times, that the data in an object meets that invariant. Maybe through sanity checks, maybe through constraints, maybe through the type system or something else.

Thinking of strong typing as a way to catch type errors at compile time instead of runtime isn't all that interesting to me. But thinking of strong typing as a way to implement Programming With Contracts, through class invariants and type conversions, is interesting to me.

Consider:

```template<typename T> locked
{
T& locked_info;

public:
locked(T& data) : locked_info(data)
{ /* yes, I'm locking *after* I've initialized, but before use; it's safe because I won't get that lock (and won't use the data) until any other locks on this data have been released -- meaning the data *should be* updated properly at that time. */
lock(locked_info);
};

operator T&()
{
return locked_info;
};

~locked()
{
unlock(locked_info);
};
};

{
return x += 2;
};

int main()
{
int y = 3;
};
```

What's the invariant for `locked`? That while the object is in existence, `locked_info` will be protected by a recursive read-write lock.

Now, yes, there are problems there. If you actually pass a `locked<int>` to `add_two_locked`, the compiler-generated copy constructor won't properly lock the temporary created, but the destructor will be called and unlock it (for proof, change the lines "`lock(locked_info);`" and "`unlock(locked_info);`" with "`std::cout << "locked/unlocked " << this << '\n';`" and see what happens).

Oh, and IIRC, the order evaluation of arguments passed to functions isn't guaranteed to follow any set pattern, meaning that you run the risk of deadlocks because you can't promise that object A will be locked before object B for a function `T add_x(locked<T> A, locked<T> B)`. Especially if you don't pass them in the same order every time you call two-argument functions.

But the concept is interesting.

 Max Lybbert Posts: 314 Nickname: mlybbert Registered: Apr, 2005
formatting Posted: Aug 15, 2006 8:31 AM
Oops. Sorry. I thought there was word-wrap on long code comments.

 Flat View: This topic has 38 replies on 3 pages [ « | 1  2  3 | » ]
 Previous Topic Next Topic