A particular class of specification language is built on Temporal Logics (TL). These logics use modality operators, namely next o, eventually (), and always □, to reason on traces of program states instead of program states. A concurrent program is considered a set of execution traces, with sometimes common prefixes (initializations, for instance), that diverge because of the different possible orderings of instructions in an interlaced execution model. Two varieties of TL are used: linear time or branching time logics, depending on the use of one or several time axes. Common logics are Linear Time Logics (LTL) and Computation Tree Logics (CTL).
With Temporal Logics, the properties of programs can be classified into two classes of properties:
• Invariance properties These express that nothing bad happens during any execution of the program; for instance, that variables always remain within some limited set or always relate by some nice and desirable property (e.g., during a bubble sort of an array of elements, some part of the array is always ordered).
• Liveness properties These express that something good will eventually happen to the program. For instance, the program eventually terminates or reaches some terminal location.
Temporal Logics can also be adapted to reason about time, especially for real-time programs. For this aim, the time dimension is either explicitly introduced (as a new variable with a particular name) or implicitly introduced by adapting the modal operators to the time dimension, restricting them, for instance, to some bounded intervals of time (for example, □^P means that P is always true within time frame [a,b]).
Was this article helpful?
Read how to maintain and repair any desktop and laptop computer. This Ebook has articles with photos and videos that show detailed step by step pc repair and maintenance procedures. There are many links to online videos that explain how you can build, maintain, speed up, clean, and repair your computer yourself. Put the money that you were going to pay the PC Tech in your own pocket.