形式化驗證 (Formal Verification) jserv 黃敬群



形式化驗證 (Formal Verification)  jserv 黃敬群
https://hackmd.io/s/H1xxp3pF0

作業系統
https://www.ptt.cc/bbs/Gossiping/M.1506802937.A.19B.html

留言

張貼留言

這個網誌中的熱門文章

Use Case Description（描述使用案例）

Use Case Description（描述使用案例） http://relyky.blogspot.tw/2010/03/use-case-description.html 此篇文章參考整理自： Writing effective Use Case Examples   http://www.gatherspace.com/static/use_case_example.html http://faculty.stut.edu.tw/~pwchen/sa&d/use-case-model.ppt http://ctl.scu.edu.tw/scutwebpub/website/DocUpload/CourseTeaching/7700011120081020155557_1.ppt 國立中山大學學位論文全文系統  http://etd.lib.nsysu.edu.tw/ETD-db/ETD-search-c/getfile?URN=etd-0710107-033445&filename=etd-0710107-033445.pdf http://docs.google.com/Doc?docid=0AXIgZjy4dqkWZGR0dzJiOTJfMTI1bWs5MjUyNw&hl=en 前言： 其實目的並非是Use Case 而是其“Description”，目的是想用此“Use Case Description”技巧來描述補捉使用者真正要的須求與規格。 主題： Use Case Description 是Use Case的內容描述，補足其極其簡單的表達，以可以明確說明該Use Case的明確目標與其執行情節的使用者觀點的流程。 Scenarios（情節) A scenario is a sequence of events that occurs during one particular execution of a system. 一個使用案例實際上不只是一序列的動作，對於各種不同的情況，其序列描述也是有很多的變化，每一序列的動作就叫稱之為情節。 For example: John Doe logs in transmits a message from John Doe to the
閱讀完整內容

列出不重複的隨機亂數

要如何列出不重複的隨機亂數呢？ 因為隨機亂數連續取值，會產生重複號碼。 要解決這個問題。 例如：程式輸出  樂透彩 選號 49個數字隨機取6個 想到三個陣列方法。 方法一：直接把全部數字49個號碼儲存在陣列裡面， 再用迴圈跑個一輪做隨機元素交換，for(i=0; i<arr.length; i++)， 迴圈裡面用一個隨機亂數取值， 指到哪個元素就 i=序列的元素跟那個隨機元素交換。 方法二：如同方法一把全部數字49個號碼儲存在陣列裡面， 再用隨機方式取出陣列裡的元素號碼，並且重新設定該元素內的 值為號碼以外的值，像是負一或其他，然後再繼續隨機取值， 如果取到的值為設定的取出重設值(代表已經選過了)，就再來一次。 方法三：使用兩個迴圈，內層迴圈裡隨機亂數取值，然後再跟之前 取過號碼的元素做比較，如果發現有一樣的號碼，可以使用i--讓 隨機亂數在重找一遍號碼，當然外面迴圈跑到越後面，後面的元素 取得的號碼跟前面重複的機會就越高。所以，這個迴圈會跑個很多次， 使用計數器，發現49取49個亂數的迴圈跑個四百多次都有可能。 方法四：已選出來的，把儲存值更改成零或負一.. Javascript使用方法二更方便，直接刪除已經取得的號碼。 <script type="text/javascript">   var arr =[];     for (i=0;i<49;i++){        arr[i]=i+1;     }   var rancodes6= new Array(6);   function ans(){     var x;     for(i=0;i<6;i++){       //這邊記得要用49-i，元素每取走一個，就少一個。     x=Math.floor(Math.random()*(49-i))     rancodes6[i]=arr.splice(x,1);   }   return rancodes6;   }     document.write(&quo
閱讀完整內容

子類別建構子super觀念

圖片
父類別子類別建構子觀念 寫程式編譯的時候出現一個 錯誤 IMPLICIT SUPER CONSTRUCTOR IS UNDEFINED FOR DEFAULT CONSTRUCTOR. MUST DEFINE AN EXPLICIT CONSTRUCTOR Implicit super constructor ZHero() is undefined. Must explicitly invoke another constructor Google找到這篇文章寫得很棒 https://ddnews.me/tech/qka5h3zp.html 關於JAVA建構子（CONSTRUCTOR）的常見問題總結 作者   六尺帳篷  - 2017-06-12 這篇文章總結了Java使用建構子中最常遇到的五個問題！ 1 為什麼調用子類的構造方法的時候，預設會調用父類的構造方法 看下面這個簡單的例子： package cc; public class Sub extends Super { public Sub() { System.out.println("Sub"); } public static void main(String[] args) { Sub sub = new Sub(); } } class Super { public Super() { System.out.println("Super"); } } Paste_Image.png 當繼承自一個類的時候，構造方法就會首先調用super()方法。如果沒有顯式的寫這個語句，那麼編譯器就會自動插入這個語句。這就是為什麼我們上面的那個例子程序會先調用super的構造方法。 但要切記，  雖然調用了父類的構造方法，但只建立了一個對象也就是子對象。 之所以要調用父類的構造方法，是因為super類可能需要建構子來初始化一些私有的成員變數。 編譯器自動插入super構造方法後，子類的建構子就會像下面這樣： public Sub(){ super()
閱讀完整內容