Abstract
We introduce two new notions of refinement for ^I¼-charts and compare them with the existing notion due to Scholz. The two notions are interesting and important because one gives rise (via a logic) to a calculus for constructing refinements and the other gives rise (via model checking) to a way of checking that refinements hold. Thus we bring together the two competing worlds of model checking and proof.
Users
Please
log in to take part in the discussion (add own reviews or comments).