Running Code

(*) Test cases have a THIS part and a THAT part such that assuming the THIS part implies the THAT part.
Test cases have explicit assumptions because assumptions should be checked.
Test cases make issues observable (both issues w.r.t. requirements and designissues).
Test cases lead to test results which are one of passing, failing, undecided or no-data.
Test cases can be in the following state: proposed, approved, extra-credit or obsoleted.