Logic of non-interacting programs and reactive systems

The notion of a program logic is introduced to denote a set of predicates which are true in different program points. The program logic can be easily constructed for different kinds of statements of an imperative or a functional language with data types except pointers. For a non-interacting program, a total correctness formula based on the program logic is defined. The rules of program correctness proof have been developed for proving the statements of various kinds. For a reactive system, the program logic is defined as a predicate on program state variables which is true after executing the current action of a trace constructed as a sequence of interleaved actions from different parallel interacting processes. An action is a maximal program fragment (without loops) of a process source code for which the program logic can be easily constructed. To analyze the behavior of a reactive system, the notion of a meta-state is introduced to denote an approximation of logic for a set of traces.