嘛。。不知不覺這門課程要結束了，那麽就再說點啥以示慶祝唄。

測試vs正確性論證

說到這個，相比很多人對此其實很有疑惑，請讓我慢慢分析。

邏輯概覽

首先我們來看看兩種方式各自的做法和流程是什麽樣的：

單元測試

在測試中，我們是這樣的一個流程

此外，為了保證測試能覆蓋到工程代碼的每一個區域，需要保證測試的覆蓋率。

正確性證明

在證明中，我們是這樣的一個流程

在這一過程中

• 基於行為分析的repOk永真性證明依賴於JSF中的modifies項
• 方法正確性將基於JSF中所描述的effects和requires項
• 各方法內其他方法的調用需要依賴被調用方法的正確性，具體來說
  • 對於系統自帶的類與方法實現一律默認正確
  • 對於其他位置的調用，正確性則依賴於其具體方法或類的正確性證明

關鍵細節

基於以上的邏輯，我們不難發現一個細節：

• 在單元測試的流程圖上，當程序通過測試後，是假定程序為正確而不是程序為正確

或者更具體地說，這裏多出了一個名為假定的字眼。

這是什麽原因的？其實說來也非常簡單——因為測試，只能證明程序有錯，而不能證明程序是對的。

雖然有大數定律的理論支撐（即只要測試集數量無限大，則必定可以覆蓋一切情況），可是實際上並不存在無限大的測試集，故測試上的死角總還是會存在的。

設一個有限集 $ T $ ，為測試集（單元測試中的測試集不可能做到無窮），而 $ S $為全集。然而，在實際情況下，可能遇到的情況常常是無窮多的，故 $ S $ 是一個無窮集。

故，$ \complement^{S}{T} $ 即為測試集沒有覆蓋到的地方。又 $ T $ 有窮， $ S $ 無窮，故 $ T \subset S $ 恒成立，$ \complement^{S}{T} \neq \emptyset $

故永遠有覆蓋不到的數據，且對於這部分無法覆蓋到的區域，是無法僅依靠測試來證明正確性的。

故基於測試的正確性驗證的嚴謹性問題是不可避免的。若要嚴格意義上地論證正確性，基於程序邏輯的正確性證明是唯一的選擇。

異與同、取與舍

在上面的分析中，我們論證了單元測試方法存在的硬傷。

然而，我們為啥還要保留這樣的方法呢？

因為，實際問題與應用大都不是一元線性的，而是時間、經濟、人力等多方面成本以及多方面效益指標所構成的高維量

其實，在工業界各類應用中，常常有以下兩種模式可以長久而穩定的存在：

• 較高的成本，絕對高的質量（或者說其質量水準具有不可替代性），但是部署門檻稍高
• 成本低廉，較高的質量，且易於廣泛普及與部署，易於操作易於維護

實際上，不僅在計算機行業，在其他工業界乃至於商業中，也常常會形成這樣兩種模式並存的局面。

而反映在軟件質量保證領域，則分別是基於程序設計邏輯的正確性證明（正確性從原理層面上就有絕對的保障，可是成本嘛，各位都寫過一次論證，體驗過其成本之高昂）和面向數據期望的單元測試（操作非常簡便，方便大範圍部署，且能覆蓋絕大部分實際情況）。

所以，在實際應用中

• 嚴格的正確性證明常常只會被運用在一些對產品質量要求絕對高的局部區域（例如航天器的核心控制程序，對錯誤的容忍度為零）
• 普通的單元測試則會被廣泛運用在一般工程項目的測試中（對錯誤有一定的容忍限度，但務必兼顧時間、經濟成本和效益，創業公司的項目中更是如此）

說到底，這兩者其實很難去嚴格區分一個優劣。很多問題，根本上還是一句話——具體問題具體分析，適合的就是對的。

OCLvsJSF

何謂OCL

OCL，英文全稱object constraint language，翻譯過來就是對象約束語言。

顧名思義，其作用在於對設計的對象進行約束，且保證不存在二義性。且實際上，OCL和UML（統一建模語言，Unified Modeling Language）捆綁使用。

異與同

從以上的一些基本概述中，我們不難發現OCL實際上和JSF有著相似之處：

• 都是對於程序設計上的約束（其中包含了類合法性、以及方法行為等要素）
• 最終目標都是描述程序設計的預期行為，作為一個統一的標準

然而進一步研究與分析，其區別也是很大的：

• 首先，OCL約束的核心對象和JSF有較大差別。JSF在圍繞方法和類，而OCL則在對象，以及對象內、對象間所包含的數據項。
• 基於以上的原因，OCL的表達能力遠遠比JSF豐富。OCL作為約束語言，可以自由地約束各處的數據項和設計規範。而JSF的不變式約束相比之下就遜色了非常多。
• 也正是由於OCL的豐富性和完備的可計算性，所以OCL完全具備類似SQL那樣的查詢能力。
• 但是，為了支撐如此龐大豐富的能力，且保證無二義性，OCL所付出的代價就是重量化。而JSF則相比之下更輕便更快捷。

而至於具體應用呢，則還是老規矩——適合的就是最好的。在不同的工程項目，不同的場合下，自然會有不同的選擇。

關於第十四次作業

UML類圖

順序圖

狀態圖

其他

知識點之間的關系

首先，我們來回顧下我們這學期四章的各個標題：

• 第一章 Java與對象（Java和面向對象基本概念入門）
• 第二章 並發與安全（多線程程序設計入門）
• 第三章 抽象與規格（規格化與整體設計進階）
• 第四章 測試與論證（工程化質量保證措施學習與體驗）

其實這很明顯，是一個循序漸進的過程，體現在兩個不同的層面上：

• 從學生學習的角度而言，知識體系是層層遞進的
• 從工業生產的角度而言，這個也很接近一個產品從設計到交付，自底向上的一個完整流程

個人收獲與小結

實際上，筆者在多年前，就已經接觸並使用了面向對象程序設計語言。

所以，實際上在這個學期，筆者的主要收獲如下：

• 通過十幾次作業對程序框架設計的反復揣摩，筆者在整體框架設計上的水平更加趨於成熟
• 更加深入的了解了嚴格工業界的一些做法（例如廣泛地規格化程序設計，以及正確性證明等）
• 此外，筆者結合之前多年的實踐經驗（理論課上講到過的坑，筆者當年幾乎全都親自踩過一遍）和對工業界的一些基本了解（筆者已經做過多筆的外包項目，目前仍在著手運營的項目也有數個），對面向對象和工程化的理解也更加深入了。

工程化的個人見解

關於工程化呢，其實說難也難，說簡單也簡單得很。

一些具體的好處呢，筆者在前三次博客作業中均有不同程度的論述（此處不再贅述）：

• 【作業】HansBug的前三次OO作業分析與小結
• 【作業2.0】HansBug的5-7次OO作業分析與小結，以及一些個人體會
• 【作業3.0】HansBug的第三次博客規格總結

不過說到底呢，其實就幾件事：

• 任何時代任何情況下，左右戰局的決定性因素，永遠是人
• 因此，工程化的一個基本思想就是以人為本
  • 從開發者角度，為開發者提供方便提高效率（無論是短期還是長期，無論是單人還是團隊，都是需要考慮的）
  • 從商業團體角度，提高整體戰鬥力，創造更大的效益和價值
  • 從用戶角度，讓用戶體驗更優（或者說給用戶提供足夠的方便），讓用戶更加願意直接或間接地掏腰包（統計意義上的）
• 此外，對於不同的解決方案，一般情況下存在即合理（或者說，對於還沒有被淘汰的解決方案，其存在終究是可以良好滿足某些場合下的需求的）。對此，我們該做的，就是具體問題具體分析，選擇在具體情況下最優的方案。

課程思考與建議

個人的思考與建議

關於這個問題，筆者在兩三個月前，就已經開始思考了。

眾所周知，面向對象課程的槽點還是不算少的。

不過，據筆者看，這些問題看似龐雜，但是只要仔細去理一理背後的邏輯關系，其實也很簡單。

筆者根據自身了解的一些事實，和大半個學期以來的觀察與分析，粗略的得到了下面的這張邏輯圖：

不過這樣一來，看似錯綜復雜的事情也就清楚了。

稍加觀察，便可以發現問題的根源——沒有一個相對公平合理的橫向比較機制。（稍微了解拓撲排序的概念，便可以得出這樣的結論，找到節點的上遊）

其實，很多同學（包括16級的和以前的學長學姐們）之前所吐槽過的問題，根源都在這邊。

假如，我們有一個很靠譜的自動化橫向比較機制

• 那麽，我們的分數將更具有梯度和區分度，且評分核心依據將是程序的真實質量
• 那麽，互測的實際門檻將可以考慮提高，互測人員的整體素質也將提高
• 那麽，基於上一條，我們將不再需要每次祈禱不遇上壞人（指的是為了自己的分數可以不要臉良心還從不痛的那種）
• 那麽，基於上一條，我們的助教們將不再需要面臨巨大的仲裁任務壓力
• 那麽，基於上一條，我們的同學們將不再需要承受等待助教仲裁的痛苦煎熬
• 那麽，我們的評測將可以考慮部分模糊化，以適應模糊化的需求
• 那麽，基於上一條，我們的同學可以不再不停地糾結需求細節（常常還是無關緊要的細節），助教們也將大大減少issue答疑時間
• 那麽，基於以上所有條，我們的同學們的整體體驗將有質的飛躍
• 那麽，基於上一條，同學們將更加願意積極努力學習這門課程

實際上，想做出改變，也並不難，比如：

• 公測不再嚴格面向bug出數據。或者至少不完全面向bug，面向bug的部分可以作為功能性弱測。
• 自動化公測引入模糊化測試。比如類似於oj中的Special Judge和提交答案題裏面的部分分機制相結合，讓程序只要不違背基本法（例如電梯不準瞬移不準分身）就能有分數，且各個水準的程序得分有梯度。
• 可以將面向bug的功能性弱測和模糊化性能強測相結合，構建出更有遊戲性的制度（也可以允許在一定時間內公測多次提交，多次刷分，追求卓越）。
• 由此，可以基於公測最終成績，設立一定的互測門檻，通過門檻者方可進入互測環節。
• 在互測環節中，可以設計類似codeforces那樣的多對多大混戰hack模式（也可以考慮待測程序不匿名，從此不再有無效作業的坑），保證互測的運氣成分降到最低。

當然以上只是一些初步構想，筆者對於這個（自認為）靠譜的新制度，已經有了更深層次的計劃和構想，更具體的計劃等細節將在另一篇文章中詳細闡述。

想對接下來的分析者們說的一些話

筆者寫到這裏之前，看過之前不少同學的一些思考與建tu議cao。

不得不說，雖然大部分的所謂分析完全流於表面，透過現象看本質的幾乎沒有（截至2018.6.25 6點整），但是，大家反映的問題，也很真實，或者說很真實地描繪了大眾水平同學眼中的面向對象課程。

說這個，其實不是想吐槽各位（實際上，筆者更希望大家能繼續描述內心的真實體驗）。

引用筆者之前說過不止一遍的一句話

沒法帶來絲毫改變，甚至只會讓事情更壞的怒火，是毫無意義的。

所以呢，希望接下來看到筆者文章的各位，能在吐槽的基礎上和自身能力所及的情況下，進行更深入的思考，可以的話也多想想到底如何才能讓事情變得更好，而不是一味地抱怨與泄私憤。

抱怨沒有用，實幹才能解決問題。

【作業4.0】HansBug的第四次面向對象課程思考