Lately, the big question in my mind, which may or may not be related to everything I wrote in the other post, is: given a piece of code, a class or a component, and its behavioral contract represented by a CSP process, that specifies not pre- and post-conditions, but specifies the behavior itself. We can tell, in static-time, if the code really do what is specified in the contract ?
Maybe, if we refine the CSP process we could tell if it really reflect the behavior of the code, but I suspect that only in some cases we could be 100% sure of that. Why do I think that ? It is known that by successively refining a CSP process we eventually get a code that implements that behavior. I say "a code" and not "the code" because there may be several "codes" that could implement such behavior. What if the code that I wanna check isn't the one that I get when I refine the CSP process ? Maybe there's a way to solve this issue or other completely diferent mecanism that could tell if a CSP process reflect the behavior of the code, but, so far, I found nothing (sugestions are welcome in the comments!!!).
All this could be useful to verify in static-time if a component really do what his contract say it does, and, based on that, we can prove many properties not only of components but of compositions as well. We could do it without knowing if the component really do what the contract specifies, but then we would have to accept the word of the contract. If the component didn't do what the contract said it does then some or all of the properties we proved regarding the component and the compositions it takes part would be false and this would reflect itself in run-time with unexpected behavior and/or wrong answers.
It would be nice too if we could, given an code, automatic generate the CSP process that specifies its behavior, kinda like a reverse refinement, but that's another history ...
Wednesday, September 15, 2010
Monday, September 6, 2010
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.
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.
Subscribe to:
Posts (Atom)