A logic for analysing actual processes of computation. It includes a representation of the idea that after every terminating computation according to some program something is true, and after some terminating computation according to a program something is true. These give operations analogous to the necessity and possibility operators of modal logic.