The Artima Developer Community
Sponsored Link

Weblogs Forum
Can Contracts be Equated with Types?

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

Welcome Guest
  Sign In

Go back to the topic listing  Back to Topic List Click to reply to this topic  Reply to this Topic Click to search messages in this forum  Search Forum Click for a threaded view of the topic  Threaded View   
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 5:33 AM
Reply to this message Reply
Advertisement
> 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 8:48 AM
Reply to this message Reply
> 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;
3
4 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 9:39 AM
Reply to this message Reply
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 11:12 AM
Reply to this message Reply
> 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 1:32 PM
Reply to this message Reply
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 2:28 PM
Reply to this message Reply
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 3:02 PM
Reply to this message Reply
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 7:42 AM
Reply to this message Reply
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 7:48 AM
Reply to this message Reply
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 4:37 PM
Reply to this message Reply
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 6:00 AM
Reply to this message Reply
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 1:22 PM
Reply to this message Reply
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 3:42 AM
Reply to this message Reply
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 11:30 AM
Reply to this message Reply
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);
  };
};
 
int add_two_locked(locked<int> x)
{
  return x += 2;
};
 
int main()
{
  int y = 3;
  add_two_locked(y);
};


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 11:31 AM
Reply to this message Reply
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 | » ]
Topic: Can Contracts be Equated with Types? Previous Topic   Next Topic Topic: Are Web Services Real? Part II


Sponsored Links



Google
  Web Artima.com   

Copyright © 1996-2014 Artima, Inc. All Rights Reserved. - Privacy Policy - Terms of Use - Advertise with Us