Formal verification and evaluation of execution time in the envelope theory

Abstract

A logic based on the envelope theory for verification of properties of programs with evaluation of rational execution time is introduced. The truth value of proposition varies with time, so that its truth set becomes naively a set of rational time where it holds We shall, however, use a function for rational time to the set of such time sets. The “envelope” is a specialization of the closure concept attached to the lattice theory. Using this logic, properties, involving time or not, of programs can be verified more precisely and easily than using conventional methods, because concrete actual values of time length are explicitly dealt with in this relatively concise formal system. Examples follow.