Software Engineering

Engineering Software Correctness

Rex Page, Engineering software correctness, Proceedings of the ACMS,PLAN 2005 Workshop on Functional and Declarative Programming in Education, September 25, 2005.

Software engineering courses offer one of many opportunities for
providing students with a significant experience in declarative
programming. This report discusses some results from taking
advantage of this opportunity in a two-semester sequence of
software engineering courses for students in their final year of
baccalaureate studies in computer science. The sequence is based
on functional programming using ACL2, a purely functional
subset of Common Lisp with a built-in, computational logic
developed by J Strother Moore and his colleagues over the past
three decades...

A JFP educational pearl with the same title and a similar abstract appears in Journal of Functional Programming (2007), 17: 675-68, but I haven't managed to access it yet.


I am still in the process of finding furniture etc. But at least I have an apartment now... Thanks for all the help and tips, guys!

Code Splitting for Network Bound Web 2.0 Applications

Code Splitting for Network Bound Web 2.0 Applications. Benjamin Livshits, Chen Ding. August 2007.

Modern Web 2.0 applications such as Gmail, Live Maps, MySpace, Flickr and many others have become a common part of everyday life. These applications are network bound, meaning that their performance can and does vary a great deal based on network conditions. However, there has not been much systematic research on trying to optimize network usage of these applications to make them more responsive for end-user interactions. Interestingly enough, code itself, usually in the form of JavaScript that runs within the client browser, constitutes a significant fraction of what needs to be transferred to the client for the application to run. Therefore, one way to significantly improve the perceived client-side performance for a range ofWeb 2.0 applications is to perform judicious decomposition — or splitting — of code and only transfer the code that is necessary just before it is needed. In this paper we propose several code splitting algorithms and explore their effectiveness at improving the responsiveness of large sophisticated Web 2.0 sites.

Once upon a time there was a lot of research on mobile code. It seemed like it was going nowhere. Then came Javascript, AJAX and Web 2.0, and in a worse-is-better fashion Javascript became the mobile code platform of choice. Maybe now is a good time to resume research on the subject...

No Name: Just Notes on Software Reuse

No Name: Just Notes on Software Reuse. Robert Biddle, Angela Martin, James Noble.

In the beginning, so our myths and stories tell us, the programmer created the program from the eternal nothingness of the void. In this essay, we recognise that programs these days are like any other assemblage, and suggest that in fact programming has always been about reuse. We also explore the nature of reuse, and claim that Components themselves are not the most important consideration for reuse; it is the end product, the composition. The issues still involve value, investment, and return. But pervasive reuse promotes a change in the method of construction of the program, and in the program itself.

This report isn't new, but seeing as it's awfully quiet around here and it does contain amusing pictures and quotations, I thought I'd share the link.

Relationally-Parametric Polymorphic Contracts

Relationally-Parametric Polymorphic Contracts, Arjun Guha, Jacob Matthews, Robert Bruce Findler, Shriram Krishnamurthi. 2007

The analogy between types and contracts raises the question of how many features of static type systems can be expressed as dynamic contracts. An important feature missing in prior work on contracts is parametricity, as represented by the polymorphic types in languages like Standard ML.

We present a contract counterpart to parametricity. We explore multiple designs for such a system and present one that is simple and incurs minimal execution overhead. We show how to extend the notion of contract blame to our definition. We present a form of inference that can often save programmers from having to explicitly instantiate many parametric contracts. Finally, we present several examples that illustrate how this system mimics the feel and properties of parametric polymorphism in typed languages.

There's a really simple and elegant idea here: you can test at runtime whether a function uses a particular argument parametrically (ie, doesn't examine it) by wrapping it in a value that raises an error if you try to use it before sending it to the function.

Domain-Specific Aspect Languages

Although the majority of work in the AOSD community focuses on general-purpose aspect languages (e.g. AspectJ), seminal work on AOSD proposed a number of domain-specific aspect languages, such as COOL for concurrency management and RIDL for serialization, RG, AML, and others. A growing trend of research in the AOSD community is returning to this seminal work

Since it seems it is DSL week around here, and since Domain-Specific Aspect Languages were not discussed here before as far as I can remember, I think now may be an appropriate time to discuss this notion.

To begin the tour, head out to the web page of the first DSAL workshop: DSAL'06 which "approached domain-specific aspect languages from a language implementation point of view, where advances in the field of domain-specific language engineering were investigated to answer the implementation challenges of aspect languages," and then move over to DSAL'07 which dealt with the design and implementation of new domain-specific aspect languages in more detail.

Designing High-Security Systems: A Comparison of Programming Languages

Designing High-Security Systems: A Comparison of Programming Languages. Ben Brosgol. STSC.

The high degree of interconnectivity in today’s computing systems and the increasing threat from technically sophisticated adversaries make security an essential requirement in modern military software. Many technical factors affect the ease or difficulty of meeting this requirement, including the programming language, the software development tools, the operating system, and the application program interface. This presentation focuses on the programming language, which is arguably the factor that a development project manager can control most directly, and assesses three major language families with respect to the criteria that a secure system must meet:

* Ada 2005 and the Ada-based SPARK language
* C and C++
* Java and its relevant extensions (Real-Time Specification for Java, Safety-Critical Real-Time Java)

The presentation focuses in particular on how modern language features (such as the data type model, Object-Oriented Programming ("OOP"), exception handling, and concurrency) affect application security, and compares the requirememts for security and for safety.

Not overly technical, but a useful summary none the less.

Automated Whitebox Fuzz Testing

Automated Whitebox Fuzz Testing. Patrice Godefroid; Michael Levin; David Molnar.

Fuzz testing is an effective technique for finding security vulnerabilities in software. Traditionally, fuzz testing tools apply random mutations to well-formed inputs and test the program on the resulting values. We present an alternative whitebox fuzz testing approach inspired by recent advances in symbolic execution and dynamic test generation. Our approach records an actual run of a program under test on a well-formed input, symbolically evaluates the recorded trace, and generates constraints capturing how the program uses its inputs. The generated constraints are used to produce new inputs which cause the program to follow different control paths. This process is repeated with the help of a code-coverage maximizing heuristic designed to find defects as fast as possible. We have implemented this algorithm in SAGE (Scalable, Automated, Guided Execution), a new tool employing x86 instruction-level tracing and emulation for whitebox fuzzing of arbitrary file-reading Windows applications.

I wonder how moving this type of system to the level of high-level programming language would impact its effectiveness.

The Expression Problem Revisited

The Expression Problem Revisited - Four new solutions using generics. Mads Torgersen. ECOOP'04.

...Over the years, many approaches to this problem have been proposed, each having different characteristics of type safety and reusability. While many of these rely on exotic or problem specific language extensions, this paper investigates the solution space within the framework of the soon-
to-be mainstream generic extensions of C# and the Java programming language.

Four new solutions are presented which, though quite different, all rely on techniques that can be used in everyday programming.

Same issue, same department (Daimi, Aarhus), different approaches.

Compared to the previous post, this paper is longer and thus perhaps easier to follow; the approach is more mainstream - and the code (in Java!) is downloadable.

The expression problem, Scandinavian style

Erik Ernst, The expression problem, Scandinavian style. MASPEGHI 2004.

This paper explains how higher-order hierarchies can be used to handle the expression problem. The expression problem is concerned with extending both the set of data structures and the set of operations of a given abstract data type. A typical object-oriented design supports extending the set of data structures, and a typical functional design supports extending the set of operations, but it is hard to support both in a smooth manner. Higher-
order hierarchies is a feature of the highly unified, mixin-based, extension-oriented kind of inheritance which is available in the language gbeta, which is itself a language that was created by generalizing the language Beta.

MASPEGHI, in case you wonder, stands for MechAnisms for SPEcialization, Generalization and inHerItance. On the site you'll also find the presentation related to the paper. And oh, gbeta is here.

I wonder what the Scala guys have to say about all this...

Combining Total and Ad Hoc Extensible Pattern Matching in a Lightweight Language Extension

Combining Total and Ad Hoc Extensible Pattern Matching in a Lightweight Language Extension. Don Syme, Gregory Neverov and James Margetson.

Pattern matching of algebraic data types (ADTs) is a standard feature in typed functional programming languages but it is well known that it interacts poorly with abstraction. While several partial solutions to this problem have been proposed, few have been implemented or used. This paper describes an extension to the .NET language F# called ``Active Patterns'', which supports pattern matching over abstract representations of generic heterogeneous data such as XML and term structures, including where these are represented via object models in other .NET languages. Our design is the first to incorporate both ad hoc pattern matching functions for partial decompositions and ``views'' for total decompositions, and yet remains a simple and lightweight extension. We give a description of the language extension along with numerous motivating examples. Finally we describe how this feature would interact with other reasonable and related language extensions: existential types quantified at data discrimination tags, GADTs, and monadic generalizations of pattern matching.

Quite related to the recent discussions of the relationships between libraries, frameworks and language features.

XML feed