形式语义01 Intro

感觉第一节课都差不多

推荐了Software Foundations，搜了一圈发现非常劝退....但还是磨磨蹭蹭看完了Lists

书上说不建议贴答案和题解，那就不贴了吧（

developing general abstractions, or building blocks, for solving problems, or classes of problems. Also considers software behavior in a rigorous and general way, to prove that programs enjoy properties

当我们提及程序的正确性时，我们在谈论什么？

How to describe meanings of programs? 含义

How to describe properties of programs? 性质

How to reason about programs? 推理

How to tell if two programs have the same behaviors or not?

How to design a new language?

How to build Bug-Free Software?

现在的软件也越来越复杂

Multi-core concurrency

Embedded software, Limited resources

Distributed and cloud computing, Network environment

Ubiquitous computing and IoT

Quantum Computing

测试的局限性

简单，容易自动化、流程化

无法保证一定没有bug

对并发(多核/网络)程序作用有限，发现的bug难以重现

Testing shows the presence, not the absence of bugs. Dijkstra

对于Crash-Proof工作，如何证明？

How to prove mathematically?

How to define "crash"?

How to prove a system is "crash-free"?

为什么要上这门课？

软件可靠性是目前严重的问题

是别人没有的优势

可以提升代码能力

更好地理解和比较编程语言

这门课很有挑战

课程内容

对现有语言的研究

讲一些定义程序行为的方法

讲一些证明程序性质的方法

如何定义性质

如何证明

Coq

可以自动化证明命题

可以自动化验证证明

我们不再需要信任证明，只需要信任证明工具，然后检验一个证明

也就是说，一个程序可以自带一个安全性proof，而运行环境自带的证明器用以验证，以此来保证程序是正确的

本文来自博客园，作者：jjppp。本博客所有文章除特别声明外，均采用CC BY-SA 4.0 协议