mesonoxian

摘要： Software Foundations Vol.I : 更多基本策略(Tactics) 本章主要內容包括： 如何在“向前證明”和“向后證明”兩種風格中使用輔助引理； 如何對數據構造子進行論證，特別是，如何利用它們單射且不交的事實； 如何增強歸納假設，以及何時需要增強； 還有通過分類討論進行論證的更 閱讀全文

摘要： Software Foundations Vol.I : 多態與高階函數(Poly) 多態 多態列表 在上一章中只使用了包含數的列表。很明顯，程序還需要能夠處理其它元素類型的列表 Inductive boollist : Type := | bool_nil | bool_cons (b : boo 閱讀全文

摘要： Software Foundations Vol.I : 使用結構化的數據(Lists) 數值序對 在 Inductive 類型定義中，每個構造子（Constructor）可以有任意多個參數 —— 可以沒有（如 true 和 O），可以只有一個（如 S），也可以更多 （如 nybble，以及下文所示 閱讀全文

摘要： Software Foundations Vol.I : 歸納證明(Induction) 歸納法證明 我們在上一章中通過基于化簡的簡單論據證明了 0 是 + 的左幺元。 我們也觀察到，當我們打算證明 0 也是 + 的 '右' 幺元時事情就沒這么簡單了 Theorem plus_n_O_firsttr 閱讀全文

摘要： 好久沒寫隨筆了,隨便投投.這里的內容主要取至《軟件基礎》第一卷https://coq-zh.github.io/. 我補充了一部分習題的答案,在https://github.com/mesonoxian-yao/softwareFoudations-volume1-coqLearn可以看看. Sof 閱讀全文

摘要： 第六章 事件處理 Qt的事件系統 事件的產生與派發 GUI應用程序是由事件(event)驅動的,點擊鼠標、按下某個按鍵、改變窗口大小等都會產生對應事件.Qt為事件處理編程提供了完善的支持.QWidget定義了大量與事件處理相關的數據類型與接口函數. 事件表示應用程序中發生的操作或變化.在Qt中,事件 閱讀全文

摘要： 第五章 模型-視圖結構 模型-視圖結構概述 模型-視圖結構是一種將數據存儲和界面分離的編程方法.模型存儲數據,視圖組件顯示模型中的數據,在視圖組件里修改的數據會被自動保存到模型里. GUI程序的主要功能是可由用戶在界面上編輯和修改數據,典型的如數據庫應用程序.在數據庫應用程序中,界面上的數據來源于數 閱讀全文

摘要： 第四章 常用界面組件的使用 在Qt類庫中,所有界面組件類的字節或間接父類都是QWidget. QWidget的父類是QObject與QPaintDevice.所以QWidget是多重繼承的類. QObject支持元對象系統,其信號與槽機制為編程中對象間通信提供了極大便利. QPaintDevice是 閱讀全文

摘要： 第九章 高級線程管理 注意:本章內容由于教材本身問題,例子存在較大問題.請自行在理解基礎上重新設計. 在大多數系統上面,為每個可以與其他任務并行執行的任務分配一個單獨的線程是不切實際的. 但線程池允許盡量充分利用硬件提供的并發性. 在線程池幫助下,可以被并發執行的任務被提交到線程池中,在線程池中被放 閱讀全文

摘要： 第八章 設計并發代碼 數據劃分工作 在處理開始前在線程間劃分數據方面,C++與MPI或OpenMP的方式較為相似. 一個任務被分成一個并行任務集,工作的線程獨立運行這些任務.并且在最后的化簡步驟中合并這些結果. 盡管這種方法是很有效的,但是只有在數據可以實現劃分時,才可如此. 考慮這樣一種情景:快速 閱讀全文