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 ...
No comments:
Post a Comment