postcondition以if语句开头，endif 后的 and result = true会报错 
