« January 2009 | Main | March 2009 »

4 posts from February 2009

February 08, 2009

Specification Languages

I have not had any instruction in formal methods, so I really didn’t encounter specification languages in my coursework, but I have read papers on proving programs including some classic papers by Hoare and Djikstra, and was familiar with Eiffel contracts.

At Harvard, I audited the first couple lectures of graduate level computer science course in Software Engineering, but never encountered modeling and specification in the initial lectures. (By the way, this instructor, a guest lecturer from industry, following custom, recounted his prior interactions with Bill Gates. He did indeed have Bill as a student, and proudly proclaimed in his opening lecture having given him a B years ago, waiting on us to form our own conclusions. Having earlier said that the Macintosh architecture was superior, his agenda was not in doubt. It didn't seem ethical for him to publish such confidential information, but then celebrities have less privacy rights.)

But, independently, I did arrive at a desire to express programming languages in a more mathematical way.

image_thumb1

My first observation was that pseudo-code programs are actually real executable programs. The obstacles typically are the use of potentially large sets used as values and the use of a search or minimization function across said sets. The pseudocode for solving 2SAT above incorporates a nondeterministic choose operation and a several set operations.

While pseudo-code programs are lacking in implementation detail needed to execute in the most efficient way, such information could actually be automatically inferred by a compiler, or, if ambiguous time-space tradeoffs are involved, specifically included by the programmer as hints or performance guarantees to the compiler (in the form of contracts or attributes). There are actually very few core algorithms, which can be permuted in many ways.

Over the past couple years, I have become better acquainted with various specification languages, typically but not exclusively used in software verification. My interests in these languages rests in the similarities to the work I am doing with my own expression language (which I will henceforth refer to as "W"), which allows me to write programs in a more succinct mathematical style yet perform efficiently.

Many of these specification languages didn't actually exist during my college years, so I can't really fault my education. Joel, some time ago, talked at Yale about a software engineering course in Dynamic Logic, which turned him of from pursuing a graduate school in Computer Science.

Last year, as part of my continual self-improvements, I proceeded through the course material on software verification. I purchased and read through Software Abstractions- Logic, Language, and Analysis, which presented the Z specification language and also encountered the Z Notation: Reference Manual online. The reading left me with the impression that, at least in some methodologies, systems are designed first with a model program, written in some specification such as Z, which is checked either manually with proof-assistants or model-checking software and then consequently or concurrently ported into actual software. My self-study involved a course syllabus, purchase books in the reading lists, reviewing course notes/presentation and other material and last a few days. It made me more acquainted with a form of temporal logic in software verification--my prior exposure with temporal logic was within the context of natural language semantics--and also with the use of mu calculus in model checking, the technology that won its pioneering researchers the ACM Turing Prize last year.

Over the years, I have subscribed to and read papers from Microsoft Research, one of the few Microsoft feeds that I still read outside of MSDN blogs. Some papers refer to Horn-clause based language, pointing the use of a Prolog-equivalent systems. Microsoft dedicates significant resources to formal methods and verification. I have come across a couple of languages for specifications: AsmL (Abstract State Machine Language) and TLA+ (Temporal Logic for Actions).

Microsoft's AsmL also shares a lot of goals that I have except that it based on operational semantics rather denotational semantics.

AsmL is useful in any situation where you need a precise, non-ambiguous way to specify a computer system, either software or hardware. AsmL specifications are an ideal way for teams to communicate design decisions. Program managers, developers, and testers can all use an AsmL specification to achieve a single, unified understanding.


One of the greatest benefits of an AsmL specification is that you can execute it. That means it is useful before you commit yourself to coding the entire system. By exploring your design, you can answer the following questions: Does it do everything you intended it to? How do the features interact? Are there any unintended behaviors?

I was not initially fond of AsmL, but I do admire its resemblance to pseudocode. Below is an example specification for in-place sorting.

image_thumb3

This program nondeterministically chooses two array items to swap until array is sorted. The choose operation closely resembles the pseudo code earlier. The loop continues until a fixed point is reached in which the next iteration of the loop produce further state changes; technically, though, the choose statement will actually fail before that occurs. By withholding detail, the algorithm can inclusively characterize both the quicksort and bubblesort algorithms according to the AsmL manual; however, these are unstable sorts which the specification disallows since distinct items that compare "equivalent" may be swapped.

I discovered TLA+ from a report that Microsoft's Oslo modeling language was reported to be based on TLA+ (Temporal Logic for Actions), although I haven't picked up on the similarities in any of the published Oslo information thus far. Joe Duffy recently also wrote about an internal research talk on TLA+ ("Math is nature's way of letting you know how sloppy your writing is") and points to a TLA+ website containing more information. TLA+ seems a bit unfriendly, and while it shares with my current work the integration of modal operators, its design shows that they are multiple ways to express the same idea. Don Box mention that one of the TLA+ architects is working in the Oslo group, but I sincerely hope that TLA+ is not Oslo’s future. It’s clear to me that Oslo will eventually evolve into richer programming model, potentially doing away with the code-behind XAML model.

My recent readings in the past few month included Software Engineering 1- Abstraction and Modelling   and Software Engineering 2- Specification of Systems and Languages which presents the RAISE specification language or RSL. I actually generally prefer this language, and seems most similar to the "W" I have been developing for so long--and initially conceived of since college.

One beneficial aspect of this exercise is seeing what operators I am missing. I noticed that RSL and W both include nondeterministic expressions. Which I have a single nondeterministic choice operator, RSL includes two with fine distinctions, and a related parallel operator. However, RSL does not have a Kleene star. I out-innovated RSL in generalizing the full regular expression operations (nondeterministic choice, Kleene star) over function composition rather than symbol concatenation. This allows me to represent and infer object invariants. I have only seen this used within the formal systems, Propositional Dynamic Logic and Interval Temporal Logic.

I have also become acquainted with other efforts such as CASL (Common Algebraic Specification Language) and VDM. VDM was the subject of a classic paper.  Developed by IBM in the 1970s and quite possibly the first specification language, there are now numerous tools including one that generates executables directly from the specification. Fred Brooks was probably influenced by this language, when writing his widely circulated paper, Mythical Man Month “No Silver Bullet,” which states that specifications, among other things, will never be a software engineering panacea.

The goal and the designs of the various specification languages diverge, but they help me to understand and refine the language W that I have built. My effort with W was inspired by the exposure to the alternative evaluation models yet common declarative presentation of the languages.

Unifying Math and Computer Science

I found articulating how and why mathematics is important in computer science challenging. It’s always been my intuition--even more so, that they are interdependent -- but can I support this claim?

The importance of math is most clear in computer graphics because of the heavy use of linear algebra in rendering and even more so in ray tracing, yet this example is unsatisfying as it seems domain-specific and not an essential to the computer science.

I have wondered whether theoretical computer science is actually the natural progression of mathematics. Mathematics has been revolutionized through automated theorem provers, computer algebra systems and other packages that have mechanized previously human activities. Computers have even been successful in proving unsolved problems. It’s certainly clear that the practice of mathematics has improved considerable, but improvements in the process of performing mathematics is not satisfying argument for the important relationship of math and computer science, as computers have revolutionized numerous unrelated fields. I also considered whether theoretical computer science notions of algorithms, computable and recursive functions, and algorithmic behavior could unify computer science with mathematics.

Yet it all seems forced. A classmate, who took 1st place nationally in the Putman Mathematics competition, remarked that CS 51 to be the hardest course he took at Harvard; this surprised me as I didn’t find the programming assignments very challenging. His mathematical prowess provided little conceptual lift in the second of two introductory computer courses at Harvard. Grasping recursion and pointers is probably predicated on knowledge about stack frames and memory addressing, which I already had, having programmed significantly in assembly language.

If math and computer science are so related, then why does much of mathematics seem irrelevant to programming, for instance, calculus and differential equations? In the 1980s, computer science was still doubted as a serious theoretical discipline.

There is actually a subfield of mathematics, discrete mathematics, specifically focused on a grab bag of mathematical topics with relevant application to computer science. If much of mathematics seems not very relevant to computer programming, it is because the study of mathematics evolved to serve the fields of physics and engineering, which deals with continuous quantities, but current computer architectures can only deal with finite quantities and computer science is still a young field with consequently less influence over the development of modern mathematics. Perhaps future architectures may support continuous bits.

Fortunately, though, much of continuous mathematics have discrete analogues. Finite calculus serves the role for discrete functions as traditional calculus serves for continuous functions. Similar techniques from integration can be applied to symbolic summation, and similar techniques from differential equation can be applied to difference/recurrences equations. The natural base for discrete function is 2 instead of e, and the discrete logarithm function is the Harmonic function.

I can point to a few reasons why mathematics and computer science haven’t mixed so well. Programming languages and compilers are designed close to the hardware, and highly constrained to physical realities of the world.

My mathematical proclivities have lead me to embrace explicitly mathematical styles of programming such as functional (Lisp, Haskell), logical (Prolog III, λ Prolog, Mercury), and equational programming(Q/Pure, Mathematica), but I have always justified such approaches in their greater expressivity and potential performance advantages through high-level optimizations. Even imperative styles of programming can be handled through conversions into functions. Speaking of imperative languages, Fortress is a new language designed for mathematicians and scientists, that shows promise in making computer programs more like mathematics.

Languages can also be evaluated symbolically, which can potentially extract out answers without performing all the computations (much as a human being can walk through code and pick out the value of variable without evaluating every expression). In this mode of evaluation, programs can utilize operators that are possible in the larger computational sense but have no natural or efficient hardware implementation: continuous data types, modal operators, nondeterminism operators, nonterminating functions.  It always seemed to me that theoretical computer science was the study of computational operators.

It’s in this case of symbolically evaluating programs that the differences between mathematics and computer science begin to disappear in which programs and expressions are the same and their evaluation yields another reduced expression.

Math & Computer Science

I have always believed in a vital relationship between mathematics and computer science. In fact, my second blog post in 2003 is also entitled “Math and Computer Science” and points to several arguments for a more incorporation of mathematics in computer science.

This belief was strengthened by being introduced to Lisp as my first formally taught computer science course, Artificial Intelligence, at Columbia University, taken during my senior year at high school. While I was already exposed to other high-level languages and assembly, the pedagogical impact of learning Lisp first is development of the strong associations between mathematics and programming such as a value-centric approach to programming. It was clear, for example, that the notion of first-class functions could provide a more generic way of programming, not to mention other ideas such as code as data, metacircularity, universal data structures. These associations were heavily strengthened by my purchase of Mathematica and my formal introduction to Prolog and ML, and their underlying mathematical foundation.

I actually became attracted to C++, because it seem like C was being enriched with a way to program in a more mathematical, high-level way with the introduction of operator overloading and OOP, but with an eye to performance. Some of this sentiment can be attributed to Stroustroup’s quasi-academic exposition of the language in the C++ Reference Manual.  I was still concerned that object-oriented mechanisms were deficient in its inability to express mathematical constructs such as set comprehensions or, more generally, a way to program using set theory, or alternatively to program in more logical style a la Prolog but without the limitations of Horn clauses and expensive searches. I wasn’t concerned as much with not be able to program in these alternate styles, as I was in the language’s inability to express mathematical notions.

At Harvard, reflecting my beliefs, I concentrated in applied math with emphasis in computer science (code words for majors and minors). I started out in computer science and applied math, but for procedural reasons and concerns that I was losing the math edge I had entering college, switched the two studies midstream—a decision I later regretted because the applied math requirements forced me to take courses outside computer science as a means of rounding out my mathematical toolset.

My knowledge in either computer science and mathematics is not as solid as I would like, as I have taken for effective half the number of courses in each discipline that a dedicated major would have taken. For instance, I audited courses in compilers and operating systems—normally two capstone CS courses--and read through the classic textbooks on the subjects, but I don’t have experience of completing projects, problem sets, and exams in those two areas.

On the other hand, some of my Applied Math courses could also fall under the Computer Science umbrella. Numerical Analysis deals with algorithms for problems of continuous mathematics. Abstract Algebra has a number of applications in in computer science such as cryptography and compression. For that course project, I wrote a full-fledged Mac application to solve the Rubik’s cube using group theory. It rendered the cube in 3d and showed all the rotations necessary to restore a cube; written using the Think Class Library framework and AppMaker designer, it was my first major application and I regret not release it as shareware.) My course in Operations Research dealt with topics like various optimization problems like linear programming, which make up Windows Solver Foundation.

Lately, I have been going through the course guides at Harvard and elsewhere to take an inventory of my knowledge set and proceed on a plan to study textbooks and online learning material from all of the missed courses in mathematics and computer science and related disciplines. Graduate courses are pedagogically efficient as the material tends to be more interesting while actively incorporating concepts introduced in undergraduate courses.

 Theory and Practice

My appreciation of mathematics in computer science was heighted by the rich theoretical treatment of computer science at Harvard. Great differences in textbooks I have surveyed (e.g., compare the “Dragon” book to other compiler books) indicate that is not true in most other schools, but as I can attest from auditing a Computational Linguistics course at UCLA, is probably true for the top schools. The Harvard CS department philosophy is to not teach technology, because such knowledge is transient, changing rapidly, in favor of more theoretical knowledge that will last a lifetime. In one course, the stated aim was to allow students to read academic papers in the field. While I agree with both of the aims, I think a general understanding of an area, beyond existing practice, is important in appreciating and advancing the field, and is not easily acquirable outside the university.

Programming languages and technology are not taught in Harvard courses, but something learned primarily on one’s own with help from “section,” hosted by teaching assistants. I find the mindset that one needs to go to school to learn technology quite amusing, but this may be the unfortunate outcome of teaching technology rather than theory.

The philosophy reflects a Harvard’s general predisposition to theory. Harvard does not have an majors in accounting, medicine, law or business, because of their practical nature. Future accountants and business students take economics, law students take government and medical students take biochemistry. Perhaps that is the right focus as an astonishing ninety percent of Harvard students eventually attain a graduate degrees. Stanford, Harvard’s polar opposite on the West Coast, was founded with a more pragmatic orientation with a more open to teaching technology. Stanford has a course on using multimedia applications and another on CS 193P: “IPhone Application Programming,” (perhaps the P refers to a professional course), neither of which would ever be admitted at Harvard, but then I noticed that Harvard's statistics department is guilty in offering Statistics 135: “Statistical Computing Software.”

Dare Osabanjo invoked a quote from Djikstra, “that computer science is no more about computers than astronomy is about telescopes” in response to Coding Horror post on the need for a more relevant computer science curriculum, which doesn’t seem to appreciate the differences between a computer science and software engineering. I am not sure that some of the suggestions such as deployment and source control, belong in either program at a top school.

I tried to dispel misconceptions of a reader, who aspired to attend a top university for very mundane programming reasons. I told him that my “Theory of Computation” course didn’t reference actual computers until the last week in which a “random access Turing machine” make theory more relevant. “Data Structures and Algorithm” included no programming, but rather was heavy on problem sets to prove properties about algorithms. My programming languages course didn’t discuss any popular programming language, but various mathematical formalisms. Harvard’s database course probably doesn’t teach SQL, but will probably give you the mathematical foundations, such as relational calculus and transaction processing, to build a database management system in the abstract.

After the heavy theory in school and being acquainted with papers on proving programs, I was somewhat disheartened by the absence and even distrust of mathematics or an academic theory in my actual work experience. Data structures were mostly limited to hash tables, arrays and linked lists, and programming felt much more like “glue” code.

I lament that I focused a lot more time on learning technology than theory during college, as I have found that technological knowledge depreciates quickly but yet never catches up to theory, yet I benefited from having used expensive $10K workstations and products so that when personal computers became unconstrained, I still came out ahead. As I have started working on advanced projects in natural language and static analysis, I found that computer science theory actually have serious applications, initially in designing my algorithms, and later, in directly representing and manipulating mathematical operators in memory.

Mathematical Programming

I began writing a post on my ideas of the relationship between mathematics and computer science, which grew very long, so I am splitting the one long post in several, and I will just include links to each post here.


Table of Contents

  1. Math and Computer Science
  2. Unifying Math and Computer Science
  3. Specification Languages