The obvious way to implement choice is to enumerate all the paths in the program and duplicate the analysis of the tail. A more efficient way would be to allow choices to be annotated with the "invariant" from the prefix that is relevant for the end, so that the could be analyzed on their own, like while loop bodies.
The obvious way to implement choice is to enumerate all the paths in the program and duplicate the analysis of the tail. A more efficient way would be to allow choices to be annotated with the "invariant" from the prefix that is relevant for the end, so that the could be analyzed on their own, like while loop bodies.