Assertion-based design (ABD) is an approach that encourages writing assertions as early as possible, preferably before coding/implementation starts.
assert(x<4); // Example imperative saftey assertion x := x + 1000; assert(x<1004); // Some programmers think this is the only form of assertion.
Programmers are used to dynamically validating imperative assertions embeded in procedural programming:
On the other hand declarative programming (aka logic programming) involves writing assertions that hold for all time.
For instance, on an indicator panel never is light A on at the same time as light B.
Declarative assertions are (conjunctions of):
All four forms can be proved by formal techniques such as pen and paper, theorem provers and model checkers.
Dynamic validation is simulation (or execution) while checking properties. This can sometimes find safety violations and, with careful constructionm detect deadlock, but it cannot prove the liveness or that safety won't be violated.
Assertions can be imported from previous designs or other parts of the same design for global consistency.
Formal proof shows up corner case problems not encountered in simulation.
A formally-verified result may be required by the customer.
2: (C) 2012-18, DJ Greaves, University of Cambridge, Computer Laboratory. |