计划覆盖

• Hoare 逻辑
• 分离逻辑
• 不变式
• 精化

原子清单