谓词精化类型

普通Int类型说明“这里存的是整数”。精化类型进一步说明“这个整数非负”或“它小于当前数组长度”。运算和分支会把已知事实积累到环境中，使用受限操作时，再检查这些事实是否足够。

编译器不需要运行所有整数输入。它把类型要求转成一个公式：如果此前的假设都成立，那么本次操作的前提是否必然成立？证明由逻辑推理或SMT求解器公理库可满足性模理论Satisfiability modulo theories · SMT判定一阶公式的布尔结构与指定背景理论是否具有同一个满足模型。完成。

给abs逐分支生成义务 ​

定义

abs(x) = if x >= 0 then x else -x

目标类型是

then分支中知道x≥0，返回表达式x可取精确类型 $\{v:Int\mid v=x\}$。为了符合目标，产生

代入v=x就得到x≥0⇒x≥0，成立。else分支知道x<0，返回−x产生

由x<0知−x>0，所以也成立。x=0只走then分支，返回0，正好满足非严格不等式。

若错误地把else写成 x-1，取x=−2，返回v=−3，违反非负条件。求解器可给出这样的反例赋值；这是规格失败的真实证人，不只是类型字符串不匹配。

数组访问需要两侧边界 ​

设不变数组a长度为n，已有n≥0。受检索引类型为

原始读取接口只接受Index(n)。考虑

readOrZero(a,n,i) =
  if 0 <= i && i < n then get(a,i) else 0

真分支环境恰有0≤i和i<n，因此实际i可通过子类型检查，get安全；假分支不读取数组。n=0时，没有整数同时满足0≤i<0，所以真分支不可达，空数组也不会被访问。

如果程序只有 if i<n then get(a,i) else 0，则n=3、i=−1是反例：上界成立但下界失败。若把条件改成 0<=i && i<=n，则n=3、i=3暴露差一错误。两例说明精化义务应来自get的完整接口，不能只检查程序恰好写出的那半条guard。

为什么先绑定中间结果 ​

在依赖结果类型中替换复杂实参时，重复出现可能影响求值或使逻辑语言变复杂。本页是纯核心，仍可采用A-normal形式：先写 let j = i+1 in get(a,j)，环境记录j=i+1，再验证0≤j<n。这样逻辑公式引用的是已经绑定的值，程序求值顺序和类型中的变量作用域都清楚。

若只有0≤i<n，不能自动推出i+1<n；边界i=n−1反驳它。额外要求i<n−1，才足以访问下一个元素。把一个表达式写成更复杂的类型，并不会替代缺失的前提。

检查过程可视为类型驱动的验证条件生成公理库验证条件生成Verification condition generation · VC generation按程序结构把带注解的正确性目标转换为有限逻辑义务，并以生成器可靠性连接公式有效性与程序语义。：普通类型规则确定结构；分支增加假设；调用处产生参数子类型义务；返回处产生结果义务。对一个义务 $H\Rightarrow P$，求解器检查 $H\wedge \mathrm{\neg }P$ 是否不可满足。只有可靠的unsat结论才能证明义务，unknown或超时不能当作通过。

指定可判定逻辑是自动化边界，不是全部程序语义的边界。数学整数的abs证明不能直接套到固定宽度有符号整数，因为最小整数取负可能溢出；数组长度若被其他线程改写，也不能继续把旧n当作当前长度。扩展语言时必须同时扩展规格与状态模型。

若加入可能发散的一般递归，可以采用“若返回则满足精化”的部分正确性解释，但不能把不返回的程序当作产生了任意命题的证明。若需要总正确性，还要独立证明终止。本文无一般递归的核心避免了这项额外责任，并没有把它藏在SMT公式里。

精化检查与自动推断也不同。给定abs的目标，两个义务已经足够；要自动发现目标，就要另选候选谓词、模板或其他抽象域。Liquid Types用有限逻辑qualifier集合组织这类推断，找不到合适精化可能是候选语言过弱，不等于原程序不安全。