This paper presents a systematic and correct design of program analysis frameworks for semantic analysis of programs. The authors introduce a formal approach to program analysis based on abstract interpretation, using lattices and predicate transformers. The paper discusses the design of a space of approximate assertions, the approximation operator, and the connection between a space of approximate assertions and a computer representation. It also examines the design of approximate predicate transformers and their correctness. The paper shows that the best approximate predicate transformer induced by a space of approximate assertions is isotone, and that this property is natural and useful for program analysis. The paper also discusses the hierarchy of approximate analyses and the design of program analysis frameworks for global program analysis. The authors conclude that the systematic design of program analysis frameworks is essential for optimizing compilers and program verification systems.This paper presents a systematic and correct design of program analysis frameworks for semantic analysis of programs. The authors introduce a formal approach to program analysis based on abstract interpretation, using lattices and predicate transformers. The paper discusses the design of a space of approximate assertions, the approximation operator, and the connection between a space of approximate assertions and a computer representation. It also examines the design of approximate predicate transformers and their correctness. The paper shows that the best approximate predicate transformer induced by a space of approximate assertions is isotone, and that this property is natural and useful for program analysis. The paper also discusses the hierarchy of approximate analyses and the design of program analysis frameworks for global program analysis. The authors conclude that the systematic design of program analysis frameworks is essential for optimizing compilers and program verification systems.