1. 程式人生 > >MIT6.031Software Construction學習筆記:(二)Specification

MIT6.031Software Construction學習筆記:(二)Specification

首先,什麼是 Specification? Specification,就是我們平時看到的API文件的說明,比如java BigInteger

why Specification

Specification 其實是作為使用者(呼叫這個API的人)和實現者(實現API的人)的一條分界線。

在這裡插入圖片描述

Specification structure

A specification of a method consists of several clauses:

  • a precondition, indicated by the keyword requires
  • a postcondition, indicated by the keyword effects

在這裡插入圖片描述

如果前提條件不滿足,也就是說呼叫者使用者的前提條件不滿足,那麼實現者可以任意處理輸出,這就相當於一個約定 是呼叫者和實現者之間的一個約定,如果呼叫者的前提不滿足,那麼呼叫者的到的輸出也是不可預料的。

在這裡插入圖片描述

所以這也就引出後面的 行為等價性(Behavioral equivalence)

也就是說實現者再實現這個方法的時候只需要滿足,呼叫者在使用這個方法的前提滿足的情況下能得到正確的輸出即可,而不需要管具體的實現,即具體的實現可以不同,可是他們表示的是同一個意思

下面的兩個方法:

static int findFirst(int[] arr, int val) {
for (int i = 0; i < arr.length; i++) { if (arr[i] == val) return i; } return arr.length; } static int findLast(int[] arr, int val) { for (int i = arr.length -1 ; i >= 0; i--) { if (arr[i] == val) return i; } return -1; }

都滿足以下規範

static int find(int[
] arr, int val) requires: val occurs exactly once in arr effects: returns index i such that arr[i] = val

aviod null

Null values are troublesome and unsafe, so much so that you’re well advised to remove them from your design vocabulary. In 6.031 — and in fact in most good Java programming — null values are implicitly disallowed in parameters and return values. So every method implicitly has a precondition on its object and array parameters that they be non-null. Every method that returns an object or an array implicitly has a postcondition that its return value is non-null. If a method allows null values for a parameter, it should explicitly state it, or if it might return a null value as a result, it should explicitly state it. But these are in general not good ideas. Avoid null.

下面是google 對guava 中null 的討論

Careless use of null can cause a staggering variety of bugs. Studying the Google code base, we found that something like 95% of collections weren’t supposed to have any null values in them, and having those **fail fast ** rather than silently accept null would have been helpful to developers.

Additionally, null is unpleasantly ambiguous. It’s rarely obvious what a null return value is supposed to mean — for example, Map.get(key) can return null either because the value in the map is null, or the value is not in the map. A null value can mean failure, can mean success, can mean almost anything. Using something other than null makes your meaning clear.

what a specification may talk about

簡單的來說就是談論 呼叫者關心的而遮蔽掉實現的細節:

A specification of a method can talk about the parameters and return value of the method, but it should never talk about local variables of the method or private fields of the method’s class. You should consider the implementation invisible to the reader of the spec.

Test & Specification

這裡簡單說其中一種觀點:

測試也是一種呼叫者呼叫,所以也應該滿足規範,也就是說測試的前提條件一定要滿足,不然不具備意義

Specifications for mutating methods

Just as we’ve said that null is implicitly disallowed unless stated otherwise, we will also use the convention that mutation is disallowed unless stated otherwise.

這一點在在引數上加 final 不就行了嗎?總的來說,specificatioin還是沒有靜態編譯檢查來的直接,有很多慣例需要實現者與呼叫者一起遵守

Exceptions

關於 exception, 我前兩天正好看見 王垠 有一篇類似的言論

This suggests a more refined rule:

  • You should use an unchecked exception only to signal an unexpected failure (i.e. a bug), or if you expect that clients will usually write code that ensures the exception will not happen, because there is a convenient and inexpensive way to avoid the exception;

  • Otherwise you should use a checked exception.

Here are some examples of applying this rule to hypothetical methods:

  • Queue.pop()throws an unchecked Empty­Queue­Exception when the queue is empty, because it’s reasonable to expect the caller to avoid this with a call like Queue.size() or Queue.isEmpty().
  • Url.getWebPage()throws a checked IOException when it can’t retrieve the web page, because it’s not easy for the caller to prevent this.
  • int integerSquareRoot(int x)throws a checked Not­Perfect­Square­Exceptionwhen x has no integral square root, because testing whether x is a perfect square is just as hard as finding the actual square root, so it’s not reasonable to expect the caller to prevent it.

Summary

  • Safe from bugs. A good specification clearly documents the mutual assumptions that a client and implementer are relying on. Bugs often come from disagreements at the interfaces, and the presence of a specification reduces that. Using machine-checked language features in your spec, like static typing and exceptions rather than just a human-readable comment, can reduce bugs still more.

  • Easy to understand. A short, simple spec is easier to understand than the implementation itself, and saves other people from having to read the code.

  • Ready for change. Specs establish contracts between different parts of your code, allowing those parts to change independently as long as they continue to satisfy the requirements of the contract.

如果規範的預定義條件能加入編譯期檢查或許能更快的定位錯誤,即 fail fast