No edit summary |
No edit summary |
||
Line 1: | Line 1: | ||
[[Category:User Manual]] | [[Category:User Manual]] | ||
{{Revision}}{{expand}} | {{Revision}} | ||
{{expand}} | |||
ProB can be used for refinement checking of B, Z and CSP specifications. Below we first discuss refinement checking for B machines. | ProB can be used for refinement checking of B, Z and CSP specifications. Below we first discuss refinement checking for B machines. | ||
=What kind of refinement is checked?= | =What kind of refinement is checked?= |
Warning This page has not yet been reviewed. Parts of it may no longer be up to date |
ProB can be used for refinement checking of B, Z and CSP specifications. Below we first discuss refinement checking for B machines.
ProB checks trace refinement. In other words, it checks whether every trace (consisting of executed operations with their parameter values and return values) of a refinement machine can also be performed by the abstract specification.
Hence, ProB does *not* check the gluing invariant. Also, PRE-conditions are treated as SELECT and PRE-conditions of the abstract machine are *not* always propagated down to the refinement machine. Hence, refinement checking has to be used with care for classical B machines, but it is well suited for EventB-style machines.