霍尔逻辑

用"前置条件 程序 后置条件"三元组推导程序正确性。这是程序验证的基础。