已验证的正确收货模块

Question

我正在制作一个注册表，该注册表在客户购买商品时产生收据。作为练习，我正考虑在Coq中制作一个收据模块，它不会产生错误的收据。总之，收据上的物品和付款总是应该为0（物品的价格> 0，付款的金额为< 0）。这是可行的，还是合理的？

做一个速写，收据将包括收到的物品和支付，像

type receipt = { 
    items : item list; 
    payments : payment list 
} 

而且会有功能添加文章和支付

add_article(receipt, article, quantity) 
add_payment(receipt, payment) 

在现实生活中，这程序当然更复杂，加入不同类型的折扣等。

当然很容易添加布尔函数check_receipt那个con公司认为收据是正确的。由于文章和付款总是在运行时添加，也许这是唯一的方法？

例子：

receipt = { 
    items = [{name = "article1"; price = "10"; quantity = "2"}]; 
    payments = [{payment_type = Cash; amount = (-20)}]; 
} 

是否清楚我想要什么？

或者更准确地证明正确的增值税计算。有几个这样的属性可以被证明。

Answer 1

您可以使用Coq来证明您的程序具有类似的属性，但我认为它并不适用于您提供的特定示例。文章和付款将在不同的时间添加，因此无法保证余额始终为零。你最后可以检查余额是否为0，但程序无论如何都必须这样做。我不认为有一种方法可以将执行时间从检查助手转移到编译时间。

我认为使用Coq来证明算法的优化和朴素实现服从相同的输入/输出关系会更有意义。如果有一种方法可以简化你的程序，也许是以性能为代价的，也许你可以使用Coq来比较两个版本。然后你会相信你在优化过程中没有引入错误。

这就是我可以说，没有看任何代码。