For instance, an inverter with input A and output B, expressed declaratively as predicates of time, can be specified as

Here the logic levels of the circuit have the same notation as the logic values in the proof system, but an approach where they are separate might is typically needed when don't care states are encompassed.

When time is quantised in units equal to a tick of the global clock then a D-type flip-flop can be expressed: Here we have dropped the implied, leading \forall t.

A complex formal specification does not necessarily describe the algorithm and hence does not describe the logic structure that will be used in the implementation. Therefore, synthesis from formal specification involves a measure of inventiveness on the part of the tool.

See whitepaper from » OneSpin-Solutions.com» Wikipedia: program refinement

(C) 2008-10, DJ Greaves, University of Cambridge, Computer Laboratory.