前往小程序,Get更优阅读体验!
立即前往
首页
学习
活动
专区
工具
TVP
发布
社区首页 >专栏 >【2023新书】程序证明,Program Proofs

【2023新书】程序证明,Program Proofs

作者头像
数据派THU
发布2023-04-08 15:10:06
3390
发布2023-04-08 15:10:06
举报
文章被收录于专栏:数据派THU
代码语言:javascript
复制
来源:专知本文为书籍介绍,建议阅读5分钟这本全面和高度可读的教科书教学生如何使用增量方法和验证感知的编程语言Dafny来形式化地推理计算机程序。

《程序证明》一书向大家展示了程序编写规范的意义,以及如何编写连接规范和程序的证明。作者以清晰和幽默的文字,概述了程序推理的基本理论,逐步建立起复杂的概念和应用,直到你对使用对象、数据结构和非微观递归等概念有全面的认知。

程序证明向学生展示了为程序编写规范意味着什么,程序满足这些规范意味着什么,以及如何编写将规范和程序联系起来的证明。K. Rustan M. Leino以清晰和幽默的笔法,首先概述了程序推理背后的基本理论。然后,他逐渐建立起复杂的概念和应用程序,直到学生们面对使用对象、数据结构和非平凡递归的真正程序。为了强调程序证明的实用性,所有材料和例子都使用验证感知的程序证明语言Dafny,但不需要事先知道Dafny。

  • 以易于阅读和学生友好的风格撰写逐步构建复杂的概念
  • 全面涵盖如何编写证明以及如何指定和验证函数式程序和命令式程序
  • 使用来自真实编程语言的真实程序文本,而不是伪代码
  • 特色引人入胜的插图和动手学习练习

https://mitpress.mit.edu/9780262546232/program-proofs/

本文参与 腾讯云自媒体同步曝光计划,分享自微信公众号。
原始发表:2023/04/05 17:00:00,如有侵权请联系 cloudcommunity@tencent.com 删除

本文分享自 数据派THU 微信公众号,前往查看

如有侵权,请联系 cloudcommunity@tencent.com 删除。

本文参与 腾讯云自媒体同步曝光计划  ,欢迎热爱写作的你一起参与!

评论
登录后参与评论
0 条评论
热度
最新
推荐阅读
领券
问题归档专栏文章快讯文章归档关键词归档开发者手册归档开发者手册 Section 归档