Catálogo de publicaciones - libros

In this talk I will review the development of the programming language Oz and the programming system Mozart. I will discuss where in hindsight I see the strong and the weak points of the language. Moreover, I will compare Oz with Alice, a typed functional language we developed after Oz.

The development of Oz started in 1991 at DFKI under my lead. The initial goal was to advance ideas from constraint and concurrent logic programming and also from knowledge representation and to develop a practically useful programming system. After a number of radical and unforeseen redesigns we arrived in 1995 at the final base language and a stable implementation (DFKI Oz). In 1996 we founded the Mozart Consortium with SICS and Louvain-la-Neuve. Oz was extended with support for persistence, distribution and modules and Mozart 1.0 was released in January 1999.

Common programming practice grants excess authority for the sake of functionality; programming principles require least authority for the sake of security. If we practice our principles, we could have both security and functionality. Treating security as a separate concern has not succeeded in bridging the gap between principle and practice, because it operates without knowledge of what constitutes least authority. Only when requests are made – whether by humans acting through a user interface, or by one object invoking another – can we determine how much authority is adequate. Without this knowledge, we must provide programs with enough authority to do anything they be requested to do.

We examine the practice of least authority at four major layers of abstraction – from humans in an organization down to individual objects within a programming language. We explain the special role of object-capability languages – such as or the proposed Oz-E – in supporting practical least authority.

The design and implementation of a capability secure multi-paradigm language should be guided from its conception by proven principles of secure language design. In this position paper we present the Oz-E project, aimed at building an Oz-like secure language, named in tribute of [MMF00] and its designers and users who contributed greatly to the ideas presented here.

We synthesize the principles for secure language design from the experiences with the capability-secure languages and the W7-kernel for Scheme 48 [Ree96]. These principles will be used as primary guidelines during the project. We propose a layered structure for Oz-E and discuss some important security concerns, without aiming for completeness at this early stage.

We present an imperative program verification system that exploits many powerful aspects of Oz. Our verification system supports an expressive assertion language for writing specifications and loop invariants. It is able to prove the correctness of elaborated imperative programs consisting of several subproblems that are checked independently. We illustrate the functionalities of our system on a few non trivial examples. Then, we explain that, using Oz constraint programming and other convenient programming mechanisms of Oz, the implementation of the system is straightforward. We also provide information about the efficiency of our implementation.

In this paper we describe our experience with how Mozart-Oz facilitates the introduction of distributed computing to students of limited programming background and how the application of a few basic programming concepts can increase the students’ comprehension of how distributed computations actually happen.

Although formal methods have the potential to greatly enhance software development, they have not been widely used in industry (particularly in the United States). We have developed a system for executing specifications by compiling them to Oz programs. Executability is a great aid in developing specifications, and also increases the usefulness of specifications by allowing them to serve as prototypes and test oracles. In this work, we describe how we have used the Oz language both as a translation target and in implementing a library of procedures used by the generated programs. Oz is ideal for our purposes, as it has allowed us to easily use declarative, concurrent constraint and graphical user interface programming together within a single framework.

Acceptance testing is formal testing conducted to determine whether or not a system satisfies its acceptance criteria and to enable the customer to determine whether or not to accept the system. An Acceptance Test Generator has been built in Oz that receives as input the formalized goal-based requirements of a system-to-be. In this framework, we motivate our choice of the Oz programming language.

Scientists from various domains resort to agent-based simulation for a more thorough understanding of complex real-world systems. We developed the Agent Visualization System; a generic system that can be added to a simulation environment to enrich it with a variety of browsers allowing the modeler to gain insight into his simulation scenario. In this paper we discuss how the various features of the Oz language and the Mozart platform aided us in the development of our system. Of particular importance were dataflow variables, high-orderness, the support for distribution and concurrency, the flexibility offered by QTk which was crucial in generating browsers whose structure is only known at run-time, in addition to a miscellany of features that were conductive to our work. We also highlight some of the implementation difficulties we faced and explain the techniques we utilized in overcoming them.

In this paper we describe two architectures and a methodology for building Mozart applications using Web technologies and tools. The first architecture is for standalone applications and the second is for web applications. An implemented example is described.

In this paper, we present QHTML, a library for building Web-based applications in Oz. QHTML provides the Oz programmer with a basic set of abstractions through which creating Web-based interfaces becomes similar to traditional graphical toolkits. In the mean time, QHTML is an experiment investigating whether a single language can replace the numerous ad-hoc combined languages/technologies currently used for building Web-based interfaces. QHTML is realized thanks to the multi-paradigm features of the Oz programming language, which supports symbolic data structures, a functional programming style, an object-oriented style and concurrency via dataflow and lightweightthreads.