Event Based Sequential Program Development: Application to Constructing a Pointer Program

In this article, I present an “event approach” used to formally develop sequential programs. It is based on the formalism of Action Systems [6] (and Guarded Commands[7]), which is encoded within B [2]. This approach has already been used to develop distributed programs [4]. In the first part, I present the basic concepts. In the second part, I develop a complete example, which is a reshaping of the Shorr and Waite marking technique [1]. This algorithm is interesting because it involves a large number of pointer manipulations.

• Type: Conference
• Year: 2003
• Where: FM
• Authors: Jean-Raymond Abrial
• Keywords: Event Approach, FM 2003, Sequential Programs, first Part