Behavioral Contracts and Behavioral Subtyping

I was reading some articles these days and one of them caught my eye. Its name is the title of the post and it talked about how to manage behavioral subtyping in the context of behavioral contracts for object-oriented languages[1]. Behavioral contracts is a type of contract that specifies pre- and post-conditions for the use of an artifact, that could be methods of a class or even a component. Behavioral subtyping is a type of subtyping that dictates that an object of subtype of T do not cause surprising behavior when treated like it is object of type T.

That being said, I read in the article, among other things, that is hard to verify statically the correctness of a behavioral contract, which means that is difficult to ensure that a given contract will never be violated in static time. Hence, we have that is difficult to determine if one type is a behavioral subtype of another type in static time.

But what if we have, say, one CSP process specifying each method of an interface/class, and the set of processes define an behavioral contract for that interface/class ? I read in another article named Conformance notions for the coordination of interaction components [2], that is possible, roughly speaking, to know if a process could be substitutable for another, without any issues like deadlocks or divergences, through refinements techniques and a model-checker, FDS for example.

If we could represent a behavioral contract of a class through CSP processes, we may be able to determine in static-time if one class is behavioral subtype of another by applying the techniques presented in the Conformance notions for the coordination of interaction components. Of course we have to analyze the amount of work (and patience) to formally specify a method and see if is worth it. Anyway, this subject is worth checking.

Maybe I'll post about this subject again, maybe not.
We'll see in the next chapters ...  :)

References:
[1] Robert Bruce Findler , Mario Latendresse , Matthias Felleisen, Behavioral contracts and behavioral subtyping, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria.
[2] Rodrigo Ramos , Augusto Sampaio , Alexandre Mota, Conformance notions for the coordination of interaction components, Science of Computer Programming, v.75 n.5, p.350-373, May, 2010.