Specifying The Fault-Intolerant Programs

In this chapter, we describe the syntax and the semantics of the input language by which developers of fault-tolerance specify the fault-intolerant program, its invariant, its specification, and the faults. The framework generates the output in the same language.