PTT推薦

Re: [問卦] 物件導向的程式語言是廢物?

看板Gossiping標題Re: [問卦] 物件導向的程式語言是廢物?作者
ousapas
(komica123)
時間推噓 推:3 噓:3 →:7

圖靈獎得主Lesslie Lamport近年來一直在推崇Formal Verification工具

TLA Plus

基本概念就是把軟體架構寫成數學狀態機定義

然後透過Temporal Logic的理論來做到100%的正確性驗證

但是TLA Plus沒有辦法直接轉換成應用程式 所以用的人一直不多

基於這個概念微軟又開發出了P語言

號稱可以兼顧Formal Verification和應用程式開發

https://github.com/p-org/P

--

※ PTT留言評論
※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 61.219.228.100 (臺灣)
PTT 網址

DPP48 07/19 06:58一大早的講什麼呢

rutsuki123 07/19 06:59先寫出一個初音我們在繼續談

johnhmj 07/19 07:00先推 不然別人以為我看不懂

ousapas 07/19 07:27就是軟體複雜到一個程度會很難測試

ousapas 07/19 07:28這時候傳統的自動化測試已經應附不了

ousapas 07/19 07:28不管加再多testcase怎麼樣都會有漏網之魚

jack1218 07/19 07:30好酷喔

jack1218 07/19 07:31這種程式怎麼寫啊

eva19452002 07/19 07:32可以用Formal Verification寫個hello

eva19452002 07/19 07:32world範例來看看嗎?

wusbetz 07/19 08:49看起來很酷,實務上不可行

CorkiN 07/19 09:08Formal驗證有些design house有在做 但我

CorkiN 07/19 09:08不太確定跟軟體的有沒有什麼不一樣