Hoare逻辑 断言语言 -用来描述程序变量满足的性质，如x==5,x+y<30 通常，断言P,O的语法同编程语言布尔表达式的 语法有些区别：如可以出现量词 ·Hoare逻辑的良形公式 -{P}C{2} -C是一段程序，P和O分别是C的前条件和后条件 -例如{x=5}x=x+1{x=6}Hoare逻辑 • 断言语言 – 用来描述程序变量满足的性质，如x==5, x+y <30 – 通常，断言P, Q的语法同编程语言布尔表达式的 语法有些区别：如可以出现量词 • Hoare逻辑的良形公式 – { P } C { Q } – C是一段程序，P和Q分别是C的前条件和后条件 – 例如 { x == 5 } x = x + 1 { x == 6 }