給定一個含數字的陣列 A [0.. N), 0 ≤ N. 其中任一個連續區段 [p..q) 的「信用」是其中正數的個數減去負數的個數：
credit p q =〈# i : p ≤ i < q : A i > 0〉-
〈# i : p ≤ i < q : A i < 0〉
請推導出一個程式，計算該陣列中「信用最高的區段」的信用，也就是
〈↑ p q : 0 ≤ p ≤ q ≤ N : credit p q〉請問如何論證：如果 0 ≤ r < dd 成立，經過這兩行程式後，0 ≤ r < dd 仍成立？
dd := dd / 2;
if dd ≤ r then r := r - dd這個例子來自 Dahl, Dijkstra & Hoare 1972 年的 Structured Programming. 書名引起我的注意：「結構化程式設計」在 70, 80 年代曾被學界、業界視為軟體危機的解方、所有人寫程式該遵守的圭臬。但每個陣營對它是什麼都各有一套解釋。數十年過去，structured programming 卻以一種不知能否算功成而退的方式被遺忘：現在的學生們自然地把程式寫成塊狀的結構，許多人甚至已經不知有 goto 這個指令。但他們沒聽過 structured programming, 對於 Dijkstra 等人當年提倡的程式推論仍一樣地陌生。
我想知道這套概念的創始者們怎麼談它，因此好奇地想讀這本書。
「讓程式能依據其結構被理解、被證明」便是我心目中的「結構化編程」。而在那個時代，他們的挑戰便是設計語言、符號，使得這種編程與推論成為可能。
「一對伴隨函子可以生出單子 (monad)」對一些人來說是「民眾知識」等級的。因為最近的一些研究，我得把相關知識整理一下，順便註記於此。
這就是語意與語法、無限與有限的差距。練習處理 regular expression 迫使你去意識到、正視這個問題。這樣的問題在 CS 的許多層面上都重複發生。
只需 O(log n) 個遞迴呼叫的費氏數演算法是怎麼來的？會比「公式解」快嗎？
因為今年做的種種改變，FLOLAC 2012 的籌備比起往年慢了一些。這兩天發現已經有人在詢問了。是的，今年 FLOLAC 照常舉辦，而且將成為大學部的正式暑修課程！也因此，FLOLAC 開課時間改為暑期後半（8月27日至9月7日）而非傳統的七月。今年的國外講者是任職於 Max Planck Institute for Software Systems 的 Arthur Charguéraud, 將為我們介紹程式語言學界影響力日增的定理證明/程式驗證工具 Coq.
雲、山、海岸線、閃電等都是自然界可看到的碎型，複雜而不規則。然而這是自然之所以美的原因。如果雲是圓形的，那多無聊。而如果數學不能捕捉自然之美，那是多麼可惜的事情。碎型理論揭去了這層神秘的面紗，告訴我們，這些自然事物的「規則」其實隱藏在另一個維度中。
為什麼這麼慢呢？Bentley 和 McIlroy 認為問題出在我們花了太多工夫把兩個白色元素一步步挪到中間。與其如此，不如先把白色元素放到兩邊去，把陣列排成「白、紅、藍、白」。等排序完成，再把白色換回中間就可以了！
這是一個 O(N-M) 的程式。如果三色數量相同，我們平均需要大約 2(N-M)/3 次交換。如果我們當初選擇從檢查 a[b-1] 開始，平均需要的交換次數則是 N-M 次。
