Dynamic Logic (modal Logic) - Test

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:

    First follow Nature, and your judgment frame
    By her just standard, which is still the same;
    Unerring Nature, still divinely bright,
    One clear, unchanged, and universal light,
    Life, force, and beauty must to all impart,
    At once the source, and end, and test of art.
    Alexander Pope (1688–1744)

    The test of a given phrase would be: Is it worthy to be immortal? To “make a beeline” for something. That’s worthy of being immortal and is immortal in English idiom. “I guess I’ll split” is not going to be immortal and is excludable, therefore excluded.
    Robert Fitzgerald (1910–1985)

    Utopias are presented for our inspection as a critique of the human state. If they are to be treated as anything but trivial exercises of the imagination. I suggest there is a simple test we can apply.... We must forget the whole paraphernalia of social description, demonstration, expostulation, approbation, condemnation. We have to say to ourselves, “How would I myself live in this proposed society? How long would it be before I went stark staring mad?”
    William Golding (b. 1911)