经过验证的正确收货模块 [英] Proven correct receipt module

问题描述

我正在开发一个收银机，当顾客购买商品时会产生收据.作为练习，我正在考虑在Coq中制作一个收据模块，该模块不会产生错误的收据.简而言之，商品和收据上的付款总和应为0(商品价格> 0且付款金额小于0).这是可行的还是明智的?

I'm working on a register which produces receipts when customers buy articles. As an exercise, I'm thinking about making a receipt module in Coq which cannot produce erroneous receipts. In short, the articles and the payments on the receipt should always sum to 0 (where articles have price > 0 and payments have amount < 0). Is this doable, or sensible?

要进行快速草绘，收据将由收据项目和付款组成，例如

To do a quick sketch, a receipt would consist of receipt items and payments, like

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

并且会有添加文章和付款的功能

And there would be functions to add articles and payments

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

在现实生活中，此过程当然会更复杂，添加不同类型的折扣等.

In real life, this procedure is of course more complicated, adding different types of discounts etc.

当然，很容易添加布尔函数check_receipt来确认收据正确.而且由于文章和付款总是在运行时添加的，也许这是唯一的方法吗?

Certainly it's easy to add a boolean function check_receipt that confirms that the receipt is correct. And since articles and payments always is added in runtime, maybe this is the only way?

示例:

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

我想知道什么吗?

或者，证明正确的增值税计算可能更有趣.有几个这样的性质可以证明.

Or maybe it's more interesting to prove correct VAT calculations. There's a couple of such properties that could be proven.

推荐答案

您可以使用Coq来证明您的程序具有类似的属性，但是我认为它不适用于您所介绍的特定示例.文章和付款将在不同的时间添加，因此无法保证余额始终为0.您可以在最后检查余额是否为0，但是程序已经必须执行该操作.我认为即使有证明助手，也无法将检查从执行时间转移到编译时间.

You can use Coq to prove your program has properties like that, but I don't think it applies to the particular example you have presented. Articles and payments would be added at different times, so there's no way of garanteeing the balance is 0 all the time. You could check at the end if the balance is 0, but the program already has to do that anyway. I don't think there's a way of moving that check from execution time to compile time even with a proof assistant.

我认为使用Coq来证明算法的优化和天真的实现遵循相同的输入/输出关系会更有意义.如果有一种简化程序的方法，也许是以性能为代价的，也许您可​​以使用Coq比较这两个版本.这样您就会确信您没有在优化过程中引入错误.

I think it would make more sense to use Coq to prove that an optimized and a naive implementation of an algorithm obey the same input / output relation. If there were a way to simplify your program, maybe at the cost of performance, maybe you could compare the two versions using Coq. Then you would be confident you didn't introduce a bug during optimization.

这就是我无需查看任何代码就能说的全部内容.

That's all I can say without looking at any code.

这篇关于经过验证的正确收货模块的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！