Test
Dynamic logic associates to every proposition an action called a test. When holds, the test acts as a NOP, changing nothing while allowing the action to move on. When is false, acts as BLOCK. Tests can be axiomatized as follows.
A8.
The corresponding theorem for is:
T8.
The construct if p then a else b is realized in dynamic logic as . This action expresses a guarded choice: if holds then is equivalent to, whereas is equivalent to BLOCK, and is equivalent to . Hence when is true the performer of the action can only take the left branch, and when is false the right.
The construct while p do a is realized as . This performs zero or more times and then performs . As long as remains true, the at the end blocks the performer from terminating the iteration prematurely, but as soon as it becomes false, further iterations of the body are blocked and the performer then has no choice but to exit via the test .
Read more about this topic: Dynamic Logic (modal Logic)
Famous quotes containing the word test:
“[17th-century] Puritans were the first modern parents. Like many of us, they looked on their treatment of children as a test of their own self-control. Their goal was not to simply to ensure the child’s duty to the family, but to help him or her make personal, individual commitments. They were the first authors to state that children must obey God rather than parents, in case of a clear conflict.”
—C. John Sommerville (20th century)
“To answer a question so as to admit of no reply, is the test of a man.”
—Ralph Waldo Emerson (1803–1882)
“He who has never failed somewhere, that man can not be great. Failure is the true test of greatness. And if it be said, that continual success is a proof that a man wisely knows his powers,—it is only to be added, that, in that case, he knows them to be small.”
—Herman Melville (1819–1891)