tsverify

证明你的TypeScript代码对每个输入都保持了它的规范，或者得到破坏它的输入。

你用普通的TypeScript写一个规范：函数的类型，以及它必须遵守的规则。Tsverify读取规范和代码 因为他们是，而问 Z3 求解器，对于每个定律，是否有输入打破了它。这个 答案是证明，或者说是输入。

// src/shipping.contract.ts: what `shipping` must do, written before the code.
import { spec } from "@emyann/tsverify"

const shippingSpec = spec<(total: number) => number>({
  // What every caller promises: a cart's total is never negative.
  requires: (total) => total >= 0,
  ensures: {
    // A law, with what it means in words: the report prints them.
    freeFrom50: {
      says: "An order of 50 or more ships free",
      holds: (total, cost) => (total >= 50 ? cost === 0 : true),
    },
    // A law alone: a smaller order pays 5.
    smallOrdersPay: (total, cost) => (total < 50 ? cost === 5 : true),
  },
})
// Its type, which the code takes.
export type ShippingSpec = typeof shippingSpec

// src/shipping.ts: the code takes its type from the spec, and imports nothing that runs.
import type { Implementation } from "@emyann/tsverify"
import type { ShippingSpec } from "./shipping.contract.ts"

export const shipping: Implementation<ShippingSpec> = (total) => (total >= 50 ? 0 : 5)

$ npx tsverify
src/shipping.ts
  ✓ shipping  2 laws  (210 ms)
    ✓ An order of 50 or more ships free  (freeFrom50, 155 ms)
    ✓ smallOrdersPay  (16 ms)

✓ 2 laws proved
  1 contract in 1 file · 1.2 s

已证明的方法 每一个 总数，不是一个样本：4999亿，50亿，100亿，以及承诺允许的其他数字。 如果没有承诺，它就会回答 e.g. (NaN)一个不是数字的总数。

现在犯每个人都会犯的错误， > 哪里 >= 本意是:

import type { Implementation } from "@emyann/tsverify"
import type { ShippingSpec } from "./shipping.contract.ts"

export const shipping: Implementation<ShippingSpec> = (total) => (total > 50 ? 0 : 5)

$ npx tsverify
src/shipping.ts
  ✗ shipping  1 counterexample, 1 proved  (177 ms)
    ✗ An order of 50 or more ships free  (freeFrom50, 99 ms)
      e.g. (50)
    ✓ smallOrdersPay  (40 ms)

✗ 1 counterexample
✓ 1 law proved
  1 contract in 1 file · 1.0 s

shipping(50) 返回 5确切数量为50的订单支付运费。反例从来不是假警报：它是假警报 在一个精确的JavaScript模型上找到，所以你的实际代码在它上面中断。该命令退出1，因此是CI步骤或编码 探员，知道任务还没完成。

一份说明书，一部分一部分地写

这就是它的全部：法律是一个返回的函数 true，从函数中键入，因此它的参数不需要 注释。包装是 { says, holds }，它也表达了它的意思，报告打印了这句话。一条关于异步的定律 代码还可以了解调用如何结束以及它所进行的调用(下面）。

为什么tsverify

• 每个输入，而不是样本。 单元测试检查您写下的输入，属性测试检查一些输入 一千个随机的。一个已证明的定律适用于它们：任意长度的数组，任意字符串，任意数字 NaN 和 -0 其中，每一个点。
• 普通的打印稿。 法律是谓词，规范是值，代码将其作为类型实现。没有新的语言， 没有注释，没有需要解析的注释。 tsc 保持代码及其规范的同步，tsverify不会在您的 应用程序。
• 关于代码作用的法律。 对于async代码和Effect程序，一个定律读取代码所做的调用，按顺序 他们的论点和结论是：“拒绝撤军没有任何意义”。
• 你可以采取行动的答案。 一个反例附带了输入，以及运行时每个调用返回的内容。一项法律 这说明该函数没有任何标记 vacuous． 完整的报告显示了该函数可以达到的结果， 每个都有一个到达它的输入。
• 循环。 它猜测循环需要的不变量，当它的猜测不够时，你就写一个。
• 它说它不能做什么。 它无法读取的代码将在该行被拒绝，取而代之的是要写的内容。它从不治疗 这部分内容不能被解读为正确，而且每一份报告都列出了它所信任的内容。

关于代码作用的法律

这里的store是一个接口，它的每个方法都是一个操作：tsverify记录了代码对它的每次调用 它。

import { type Rejects, spec } from "@emyann/tsverify"

/** Where names are kept. Each method is an operation: tsverify records every call. */
export interface Names {
  readonly get: (id: string) => Rejects<string | undefined, Error>
  readonly set: (id: string, name: string) => Rejects<void, Error>
}

const renameSpec = spec<(names: Names, id: string, name: string) => Rejects<boolean, Error>>({
  ensures: {
    // An empty name never reaches the store: not a single call.
    emptyNameTouchesNothing: (_names, _id, name, _out, calls) => (name === "" ? calls.length === 0 : true),
  },
})
export type RenameSpec = typeof renameSpec

import type { Implementation } from "@emyann/tsverify"
import type { RenameSpec } from "./rename.contract.ts"

export const rename: Implementation<RenameSpec> = async (names, id, name) => {
  const current = await names.get(id)
  if (current === undefined || name === "") return false
  await names.set(id, name)
  return true
}

$ npx tsverify src/rename.ts
src/rename.ts
  ✗ rename  1 counterexample  (165 ms)
    ✗ emptyNameTouchesNothing  (95 ms)
      e.g. ({}, "", "")
      where names.get gave ""

✗ 1 counterexample
  1 contract in 1 file · 0.9 s

如果名称为空，代码仍然会在说no之前读取存储。先查名字，就证明了这个定律：

import type { Implementation } from "@emyann/tsverify"
import type { RenameSpec } from "./rename.contract.ts"

export const rename: Implementation<RenameSpec> = async (names, id, name) => {
  if (name === "") return false
  const current = await names.get(id)
  if (current === undefined) return false
  await names.set(id, name)
  return true
}

$ npx tsverify src/rename.ts
src/rename.ts
  ✓ rename  1 law  (205 ms)
    ✓ emptyNameTouchesNothing  (136 ms)

✓ 1 law proved
  1 contract in 1 file · 0.9 s

效果程序也以同样的方式工作，它们的服务就是操作。影响项目）。 examples/hono Hono中的用户API是否构建了两次，使用异步处理程序和Effect处理程序，都得到了证明 违反同样的法律。

它与性能测试相比如何

在相同的定律上，经过良好调优的属性测试人员经常会发现相同的错误。在 一个基准 在一个有10个状态的状态机中植入了17个bug 求解器和属性测试（种子随机输入，偏向于边缘情况）都捕获了相同的10。的区别 在另外7个。求解器解释了每一个：2个是无害的，对每个输入都证明了它们的行为和原来的一样， 还有5个从法律漏洞中溜走，每个都有一个输入。随机测试没有发现它们。

因此，获得的好处不是捕获更多的错误，而是更多的证明而不是样本，以及关于规范的答案 它本身：它的弱点在哪里，法典能达到什么程度，哪些法律没有规定。

安装

npm install --save-dev @emyann/tsverify  # add `effect` for Effect programs
npx tsverify                             # every contract under the current folder
npx tsverify --watch                     # again on every save, until all is proved

它需要Node 24.16或更高版本，并自带 typescript 和 z3-solver． 它读取导入的每个文件 @emyann/tsverify，不管它叫什么；这些页面命名一个规范文件 *.contract.ts，测试运行器不会将其误认为是测试。

你的 tsconfig.json 需要 strict (或者至少 strictNullChecks)，以及读取包的模块解析 exports： nodenext， node16 或者 bundler． 这些例子使用的是：

{
  "compilerOptions": {
    "target": "es2023",
    "module": "nodenext",
    "moduleResolution": "nodenext",
    "strict": true,
    "noEmit": true,
    "allowImportingTsExtensions": true,
    "skipLibCheck": true,
    "types": []
  }
}

答案是什么？

只有当每个law都为时，该命令才为0 proved. 读报告 每有判决，怎么办 关于它，还有 --json 为工具。

了解更多

• 编写规范：纯函数，异步代码及其调用，已经存在的代码。
• 读报告：每一个判决和下一步该做什么；命令及其退出码。
• 影响项目：服务作为操作，输入错误，它读取的表单。
• 循环和证明代码：它猜测的不变量，和 invariant， assert 和前题。
• 它所读的，拒绝和信任：它读取的TypeScript，每个拒绝和它的修复， assume.
• 这些例子说明了什么：每项测量，除性能测试外。
• 它是如何工作的：每个检查的两面，以及代码如何变成Z3。

状态

原型：版本0.1.0，其API可能在1.0之前更改。这些页面中的每个示例都由其测试运行 包括所示的输出。在你依赖它之前，最重要的是：

• 实参有自己的类型代码只在它规定的地方抛出。在程序的边缘，选中 首先是值（比如使用模式）。
• 你用什么申报？ assume 是可信的没有得到证实，而且每份报告都列出了这一点。
• 一个循环被带到终点。
• 这些例子都是作者自己的因此，它们显示了tsverify读取和捕获的内容，而不是它如何处理代码 另一个人写道。

所有的警告 · 接下来会发生什么 · 贡献

许可证

麻省理工学院