形式語義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 協定