经过验证的正确收货模块 [英] 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屋!