Programmed Strategies for Program Verification

Plover is an automated property-verifier for Haskell programs that has been under development for the past three years as a component of the Programatica project. In Programatica, predicate definitions and property assertions written in P-logic, a programming logic for Haskell, can be embedded in the text of a Haskell program module. Properties refine the type system of Haskell but cannot be verified by type-checking alone; a more powerful logical verifier is needed.Plover codes the proof rules of P-logic, and additionally, embeds strategies and decision procedures for their application and discharge. It integrates a reduction system that implements a rewriting semantics for Haskell terms with a congruence-closure algorithm that supports reasoning with equality. It employs strategies such as structure splitting and case analysis to explore alternative valuations of expressions of type Bool or other finite data types, but these strategies can lead to exponential growth of terms and must be employed cautiously.Plover itself is written in Stratego, which has proven to be a powerful language tool for implementating a verifier. We discuss the design and implementation of some strategies that enable Plover to comprehend Haskell and verify many valid property assertions.     

Haskell语言的高阶特性及其应用

Haskell语言的高阶特性使笔者在开发软件时受益匪浅,但很遗憾,目前国内同行应用这一语言的人非常少。本文介绍Haskell语言的高阶特性,并通过几个与树相关的例子,阐述如何利用Haskell语言的高阶特性来编写功能强大但却简短漂亮的程序。     

函数式语言泛型特性的研究与实现

对于泛型程序设计来说,类型的参数化多态是其理论框架,参数化多态引入了类型变量,使得类型参数化,支持类型上的抽象,从而可以大大提高软件的复用程度。泛型编程思想已经在多种语言中得到运用,并已取得了不小的成果。在函数式语言上进行泛型的研究与应用,Haskell语言是函数式语言中较为经典的一种语言,它的计算模型简单,语法清晰,易于编写,易于维护,拥有很大的发展空间。利用一些规则对Haskell语言的语法进行相关扩展,同时引入泛型的思想,研究与运用定义泛型函数的方法,在Haskell语言上实现了泛型功能。     

On building cyclic and shared structures in Haskell

We demonstrate how to build certain cyclic and other multi-linked structures in the lazy functional programming language Haskell. No explicit pointers are used in these constructions. Each task is accomplished by starting with a suitable specification and then calculating the required program.     

Object-Oriented Style Overloading for Haskell (Extended Abstract)

Haskell has a sophisticated mechanism for overloading identifiers with multiple definitions at distinct types. Object-oriented programming has a similar notion of overriding and overloading for methods names. Unfortunately, it is not possible to encode object-oriented overloading directly using Haskell overloading. This deficiency becomes particularly tiresome when Haskell programs wish to call methods imported from an object-oriented library.We present two refinements of Haskell's type class system: Closed classes and overlapping instances. We demonstrate how we may exploit the refined system so as to be able to encode object-oriented classes within Haskell. This encoding allows us to mimic, within Haskell, the overloading resolution rules employed by object-oriented languages without the need for additional type annotations or name mangling. As a consequence, object-oriented class libraries are very convenient to import and use within Haskell.We thank Don Syme, Nick Benton, Andrew Kennedy, and the anonymous reviewers, for many helpful comments.     

Pardis: a process calculus for parallel and distributed programming in Haskell

Parallel programming and distributed programming involve substantial amounts of boilerplate code for process management and data synchronisation. This leads to increased bug potential and often results in unintended non-deterministic program behaviour. Moreover, algorithmic details are mixed with technical details concerning parallelisation and distribution. Process calculi are formal models for parallel and distributed programming but often leave details open, causing a gap between formal model and implementation. We propose a fully deterministic process calculus for parallel and distributed programming and implement it as a domain-specific language in Haskell to address these problems. We eliminate boilerplate code by abstracting from the exact notion of parallelisation and encapsulating it in the implementation of our process combinators. Furthermore, we achieve correctness guarantees regarding process composition at compile time through Haskell’s type system. Our result can be used as a high-level tool to implement parallel and distributed programs.     

A Monadic Semantics for Core Curry

We give a deterministic, big-step operational semantics for the essential core of the Curry language, including higher-order functions, call-by-need evaluation, non-determinism, narrowing, and residuation. The semantics is structured in modular monadic style, and is presented in the form of an executable interpreter written in Haskell. It uses monadic formulations of state, non-determinism, and resumption-based concurrency.     

Programmable Rewriting Strategies in Haskell: — White Paper —

Programmable rewriting strategies provide a valuable tool for implementing traversal functionality in grammar-driven (or schema-driven) tools. The working Haskell programmer has access to programmable rewriting strategies via two similar options: (i) the Strafunski bundle for generic functional programming and language processing, and (ii) the “Scrap Your Boilerplate” approach to generic functional programming. Basic rewrite steps are encoded as monomorphic functions on datatypes. Rewriting strategies are polymorphic functions composed from appropriate basic strategy combinators.We will briefly review programmable rewriting strategies in Haskell. We will address the following questions:

• What are the merits of Haskellish strategies?

• What is the relation between strategic programming and generic programming?

• What are the challenges for future work on functional strategies?

Arrows for secure information flow

This paper presents an embedded security sublanguage for enforcing information-flow policies in the standard Haskell programming language. The sublanguage provides useful information-flow control mechanisms including dynamic security lattices, run-time code privileges and declassification all without modifying the base language. This design avoids the redundant work of producing new languages, lowers the threshold for adopting security-typed languages, and also provides great flexibility and modularity for using security-policy frameworks.The embedded security sublanguage is designed using a standard combinator interface called arrows. Computations constructed in the sublanguage have static and explicit control-flow components, making it possible to implement information-flow control using static-analysis techniques at run time, while providing strong security guarantees. This paper presents a formal proof that our embedded sublanguage provides noninterference, a concrete Haskell implementation and an example application demonstrating the proposed techniques.¹     

Proofs, Programs, Processes

The objective of this paper is to provide a theoretical foundation for program extraction from inductive and coinductive proofs geared to practical applications. The novelties consist in the addition of inductive and coinductive definitions to a realizability interpretation for first-order proofs, a soundness proof for this system, and applications to the synthesis of non-trivial provably correct programs in the area of exact real number computation. We show that realizers, although per se untyped, can be assigned polymorphic recursive types and hence represent valid programs in a lazy functional programming language such as Haskell. Programs extracted from proofs using coinduction can be understood as perpetual processes producing infinite streams of data. Typical applications of such processes are computations in exact real arithmetic. As an example we show how to extract a program computing the average of two real numbers w.r.t. the binary signed digit representation.     

Comparing Parallel Functional Languages: Programming and Performance

This paper presents a practical evaluation and comparison of three state-of-the-art parallel functional languages. The evaluation is based on implementations of three typical symbolic computation programs, with performance measured on a Beowulf-class parallel architecture.We assess three mature parallel functional languages: PMLS, a system for implicitly parallel execution of ML programs; GPH, a mainly implicit parallel extension of Haskell; and Eden, a more explicit parallel extension of Haskell designed for both distributed and parallel execution. While all three languages employ a completely implicit approach to communication, each language takes a different approach to specifying and controlling parallelism, ranging from explicit identification of processes as language constructs (Eden) through annotation of potential parallelism (GPH) to automatic detection of parallel skeletons in sequential code (PMLS).We present detailed performance measurements of all three systems on a widely available parallel architecture: a Beowulf cluster of low-cost commodity workstations. We use three representative symbolic applications: a matrix multiplication algorithm, an exact linear system solver, and a simple ray-tracer. Our results show how moderate speedups can be achieved with little or no changes to the sequential code, and that parallel performance can be significantly improved even within our high-level model of parallel functional programming by controlling key aspects of the program such as load distribution and thread granularity.     

Lambada, Haskell as a better Java

The Lambada framework provides facilities for fluid interoperation between Haskell (currently both Hugs and GHC using non-Haskell98 extensions) and Java. Using Lambada, we can call Java methods from Haskell, and have Java methods invoke Haskell functions. The framework rests on the Java Native Interface (JNI). The Lambada release includes a tool for generating IDL from Java.class files (using reflection), which is fed into our existing HDirect to generate Haskell-callable stubs.     

Using Maude and Its Strategies for Defining a Framework for Analyzing Eden Semantics

Eden is a parallel extension of the functional language Haskell. On behalf of parallelism Eden overrides Haskell's pure lazy approach, combining a non-strict functional application with eager process creation and eager communication. We desire to investigate alternative semantics for Eden in order to analyze the consequences of some of the decisions adopted during the language design. In this paper we show how to implement in Maude the operational semantics of Eden in such a way that semantic rules can be modified easily. Moreover, other semantic features can be implemented by means of parameterized modules that allow to instantiate in different ways several parameters of the semantics but without modifying the semantic rules.     

An experimental evaluation of a higher-ordered-typed-functional specification-based test-generation technique

HOTTest is a model based test automation technique of software systems based on models of the system described using HaskellDB. HaskellDB is an embedded domain specific language derived from Haskell. HOTTest enforces a systematic abstraction process and exploits system invariants for automatically producing test cases for domain specific requirements. Use of functional languages for system modeling is a new concept and hence HOTTest is subject to concerns of usability, like any other new technique. Also, the syntax and the declarative style of Haskell based languages make them difficult to learn. Similar concerns can be raised for HOTTest as it shares the same syntax with Haskell. In this paper we describe an experiment designed to study the usability of HOTTest and to compare it with existing model based test design techniques. The results show that HOTTest is more usable than the traditional technique and demonstrate that the test suites produced by HOTTest are more effective and efficient than those generated using the traditional model based test design technique. Editor: James Miller     

Warm fusion in Stratego: A case study in generation of program transformation systems

Stratego is a domain-specific language for the specification of program transformation systems. The design of Stratego is based on the paradigm of rewriting strategies: user-definable programs in a little language of strategy operators determine where and in what order transformation rules are (automatically) applied to a program. The separation of rules and strategies supports modularity of specifications. Stratego also provides generic features for specification of program traversals. In this paper we present a case study of Stratego as applied to a non-trivial problem in program transformation. We demonstrate the use of Stratego in eliminating intermediate data structures from (also known as deforesting) functional programs via the warm fusion algorithm of Launchbury and Sheard. This algorithm has been specified in Stratego and embedded in a fully automatic transformation system for kernel Haskell. The entire system consists of about 2600 lines of specification code, which breaks down into 1850 lines for a general framework for Haskell transformation and 750 lines devoted to a highly modular, easily extensible specification of the warm fusion transformer itself. Its successful design and construction provides further evidence that programs generated from Stratego specifications are suitable for integration into real systems, and that rewriting strategies are a good paradigm for the implementation of such systems. This revised version was published online in June 2006 with corrections to the Cover Date.     

Comonads理论及其在函数式程序语言Haskell中的应用

函数式程序语言Haskell中的Monads理论在描述上下文依赖计算等方面存在一定的不足。作为Monads的范畴论对偶概念,Comonads理论可以有效地提高Haskell对上下文依赖计算的描述能力。首先给出Comonads的范畴论定义和性质,以及Comonads在Haskell的具体实现;接着探讨Comonads的CoKleisfi三元组和CoKleisli范畴,通过实例说明如何将其应用于上下文依赖计算的描述和推理中;最后进一步研究Comonads与Monads之间的分配律,指出如何通过分配律将效果计算与上下文依赖计算有机地融合起来。     

防火墙规则间包含关系的解析方法

针对防火墙规则集中规则间的相互关系难以把握,从而导致防火墙无法正确地过滤数据包的问题,提出了一种基于集合理论的规则间包含关系的解析方法.该方法在不考虑规则动作的情况下,基于集合理论的包含关系来解析和分类规则之间的关系,简化了分析规则间相互关系的过程.并且使用高效的函数式编程语言Haskell实现了所提出的方法,整体代码简洁、易于维护和扩展.实验结果表明,对于中小规模的防火墙规则集,能够快速而有效地解析规则间的包含关系,并且能够为后续的规则间的异常检测提供重要的依据.     

The music of streams

Data streams make preeminent instruments for playing certain classical themes from analysis. Complex networks of processes, effortlessly orchestrated by lazy evaluation, can enumerate terms of formal power series ad infinitum. Expressed in a language like Haskell, working programs for power-series operations are tiny gems, because the natural programming style for data streams fits the mathematics so well—often better than time-honored summation notation.