Review Recall the we use the following logic: Goals: G::=LI true GiAG2 H>G VX.G Hypotheses: H :=L true HiA H2 Literals: L:=p(E1,....Ek) Expressions: E ::nI f(E1,...Em) This is sufficient for VCGen iff: The invariants,preconditions and postcond.are all from H Prof.Necula CS 294-8 Lecture 11 2Prof. Necula CS 294-8 Lecture 11 2 Review • Recall the we use the following logic: Goals: G ::= L | true | G1  G2 | H  G | x. G Hypotheses: H ::= L | true | H1  H2 Literals: L ::= p(E1 , …, Ek ) Expressions: E ::= n | f(E1 , …, Em) • This is sufficient for VCGen iff: – The invariants, preconditions and postcond. are all from H