Skip to Content
深入理解運算原理|從簡單的機器到無所不能的程式
book

深入理解運算原理|從簡單的機器到無所不能的程式

by Tom Stuart
November 2017
Beginner to intermediate
344 pages
7h 2m
Chinese
GoTop Information, Inc.
Content preview from 深入理解運算原理|從簡單的機器到無所不能的程式
318
|
9
我們從型別系統獲得的任何資訊都不能盡信,而且在決定要相信多少的時候,也必須注
意它的極限。成功執行程式的靜態語意並不代表『這個程式一定能運作』,只是『這個
程式的確不會以特定的方式失敗』。能有這樣的自動化系統的確很棒,因為它可以告訴
我們程式沒有任何可能的臭蟲或錯誤,但正如我們在第 8 章所看到的,事情偏偏就是那
麼不巧。
應用
本章描繪了抽象解譯的基本概念(使用低廉的近似來學習昂貴運算的行為),並示範了
簡單的型別系統,作為近似對分析程式是如何有用的範例。
我們對抽象解譯的討論相當非正式。嚴格來說,抽象解譯是一種正式且正規的數學技
術,在這種技術裡將相同語言的不同語意,透過將一組具體的值轉換成抽象的值(反之
亦然)的函數相互連接,進而能以具體的值來瞭解抽象程式的結果和特性。
這種技術最知名的業界應用是 Astrée 靜態分析儀(
http://www.astree.ens.fr/
),它使用抽
象解譯來自動查驗 C 程式沒有諸如除以零、陣列索引超越邊界、整數溢位等執行階段
錯誤。Astrée 已經用在驗證空中巴士 A340 A380 飛機的飛行控制軟體,以及運補到
國際太空站的
Jules Verne
ATV-001 飛行任務的自動對接軟體。抽象解譯顧及萊斯定理
的方式,就是提供安全的近似,而非肯定的答案,所以 Astrée 回報的執行階段錯誤,
實際上可能不存在(誤警 [
false alarm
]);實際上,它的抽象體精確度在驗證 A340 軟體
時,已足以避免任何誤警。
SIMPLE ...
Become an O’Reilly member and get unlimited access to this title plus top books and audiobooks from O’Reilly and nearly 200 top publishers, thousands of courses curated by job role, 150+ live events each month,
and much more.

Read now

Unlock full access

More than 5,000 organizations count on O’Reilly

AirBnbBlueOriginElectronic ArtsHomeDepotNasdaqRakutenTata Consultancy Services

QuotationMarkO’Reilly covers everything we've got, with content to help us build a world-class technology community, upgrade the capabilities and competencies of our teams, and improve overall team performance as well as their engagement.
Julian F.
Head of Cybersecurity
QuotationMarkI wanted to learn C and C++, but it didn't click for me until I picked up an O'Reilly book. When I went on the O’Reilly platform, I was astonished to find all the books there, plus live events and sandboxes so you could play around with the technology.
Addison B.
Field Engineer
QuotationMarkI’ve been on the O’Reilly platform for more than eight years. I use a couple of learning platforms, but I'm on O'Reilly more than anybody else. When you're there, you start learning. I'm never disappointed.
Amir M.
Data Platform Tech Lead
QuotationMarkI'm always learning. So when I got on to O'Reilly, I was like a kid in a candy store. There are playlists. There are answers. There's on-demand training. It's worth its weight in gold, in terms of what it allows me to do.
Mark W.
Embedded Software Engineer

You might also like

JSON實務手冊

JSON實務手冊

Tom Marrs

Publisher Resources

ISBN: 9789864766000