Tomohiro Oda
email: tomohiro@sra.co.jp

Gaël Dur
email: dur.gael@shizuoka.ac.jp

Stéphane Ducasse
email: stephane.ducasse@inria.fr

Hugo Daniel Macedo

Implementation-First Approach of Developing Formal Semantics of a Simulation Language in VDM-SL

Formal specification is a basis for rigorous software implementation. VDM-SL is a formal specification language with an extensive executable subset. Successful cases of VDM-family including VDM-SL have shown that producing a well-tested executable specification can reduce the cost of the implementation phase. This paper introduces and discusses the reversed order of specification and implementation. The development of a multi-agent simulation language called RE:MOBIDYC is described and examined as a case study of defining a formal specification after initial implementation and reflecting the specification into the implementation code.

Introduction

Lightweight formal methods are partial applications of formal methods so that a formal specification of the whole or a part of the software system provides the implementation with clear goal conditions of its functionality [START_REF] Fitzgerald | VDMTools: Advances in Support for Formal Modeling in VDM[END_REF][START_REF] Agerholm | A Lightweight Approach to Formal Methods[END_REF]. A formal specification consists of concise and unambiguous definitions of the system's functions which allow implementors to focus on the correctness and efficiency of the implementation. VDM-SL [START_REF] Larsen | VDM-10 Language Manual[END_REF] is one of the oldest formal specification languages still in practical use. VDM-SL has an extensive subset that can be executed by interpreters, which enables unit testing of specifications. Successful cases of the VDM-family [START_REF] Fitzgerald | Balancing Insight and Effort: the Industrial Uptake of Formal Methods[END_REF][START_REF] Oda | ViennaVM: a Virtual Machine for VDM-SL development[END_REF] have shown that producing a well-tested executable specification benefits the implementation phase. Unit testing ensures that the algorithms defined in the specification work as expected in the test cases. Test cases for the VDM specification can also be rewritten in implementation languages so that the implementation works the same as the executable specification.

While the specification is deemed to be written before the implementation in traditional views of software lifecycles, the implementation sometimes precedes the specification in practice. Development of a GUI application is sometimes driven by GUI prototypes before the developers capture the whole required functionality of the application. This then raises the following questions: Is it worth writing a formal specification even if the implementation is already running? How much does it cost to write a concise specification based on an exploratory implementation?

This paper describes a development process where the formal specification was written after the implementation. RE:MOBIDYC [START_REF] Oda | re: Mobidyc-reconstructing modeling based on individual for the dynamics of community[END_REF] is a multi-agent simulation system for population dynamics in biology. Defining the operational semantics of the modeling language in VDM-SL was planned from the beginning of the development. Although the implementation phase typically follows the formal specification phase, the implementation of a GUI-based environment including an interpreter was started without the formal semantics. Domain-specific features in the modeling languages, such as life-history stages, moulting and reproduction, were implemented and evaluated in exploratory manners involving biologists. The formal semantics was defined after the language features had become stable. The formal specification was refactored into a more concise presentation and the implementation was improved by reflecting the refactored specification.

In Section 2, the design and implementation of RE:MOBIDYC and its modeling language are explained. Its development process will be described in Section 3. Findings from the development will be discussed in Section 4, and Section 5 concludes the paper.

RE:MOBIDYC and its modeling Language

RE:MOBIDYC is a multi-agent simulation platform for the scientific study of biology and ecology, built upon Pharo [START_REF] Oda | re: Mobidyc-reconstructing modeling based on individual for the dynamics of community[END_REF]. In multi-agent simulation, agents with simpler definitions interact with each other to exhibit complex phenomena.

The following are RE:MOBIDYC's design principles to support the user's tasks.

DP1. The language should not impose imperative programming. DP2. The language must guarantee the computation always terminates or aborts. DP3. The system should provide GUI-based interfaces to define a model. DP4. The language should provide semantic checking based on measurement units. DP5. The system should record all attribute variables of all agents at all time steps. DP6. The system should always produce the same result from the same model.

DP1 and DP2 are to support biologists and ecologists who are not necessarily familiar with imperative programming languages. In general, it is hard to verify whether or not an imperative program with assignments and conditional loops implements the mathematical model at hand. The termination property is also hard to verify. DP2 implies that the language will not be Turing complete. In return, the model will be free of incidental infinite loops. DP3 and DP4 help the user to reduce the burdens of syntax and semantic errors in the model. Fig. 1 shows the GUI-based modeler for DP3. The basic idea of DP4 is to use measurement units as static types to detect semantically ill-formed expressions in the model. DP5 and DP6 are for the verifiability and reproducibility of simulation results to make the simulation more useful as a tool for scientific research. RE:MOBIDYC is built upon Pharo [START_REF] Bergel | Deep Into Pharo[END_REF][START_REF] Black | Pharo by Example[END_REF], a modern dynamic object-oriented language derived from Smalltalk, which provides a flexible and immersive programming environment on macOS, Linux and Windows systems. Fig. 2 illustrates the software configuration of the RE:MOBIDYC simulation environment. It shows three major UI elements, namely text-based modeler, GUI-based modeler, and Observatory which runs a simulation and visualises the result. Functional components operated by the user such as type checker and interpreter are also built on the fundamental elements such as the abstract syntax tree (AST), measurement units and the memory model. Among the UIs, textbased modeler is provided as a backup to GUI-based modeler UI in the case that the model definition files are broken for some reason. The scope of the formal specification in VDM-SL was limited to the components enclosed by the red lines in Fig. 2. The specification phase was started after their first implementation in Pharo had been done and the language had become stable enough.

The development of RE:MOBIDYC required a GUI-based modeling environment and exploratory design of the modeling language because the language must be validated by experts from biology and ecology. Pharo's dynamic nature enables agile prototyping to quickly develop the GUI-based modeler and the interpreter. The modeling language and its interpreter including the memory model were developed with the implementation in Pharo first, and then its formal semantics was defined in VDM-SL. The development is still ongoing in both implementation and formal semantics as an open-source project.

Overview of the Language Design

RE:MOBIDYC is designed to be friendly to mathematical modelers in biology and ecology, demanding less programming skills [START_REF] Oda | re: Mobidyc-reconstructing modeling based on individual for the dynamics of community[END_REF]. The models in RE:MOBIDYC are constructed in the declarative manner so that the models look more like definitions of numeric sequence in the form of recurrence relations rather than a series of imperative statements. Fig. 3 illustrates the major constructs of the modeling language. Agent, action, task, and attribute are the most significant constructs in the modeling language. RE:MOBIDYC has three kinds of agents: World, Patch, and Stage. World is the agent that represents the global environment, and a Patch represents the local environment. A stage is also called an animat, which has two attributes x and y so that they can move around in a two-dimensional space. A stage represents a life-history stage of an individual life such as larva, juvenile, and adult which together represent an individual. An individual is modeled as an instance of a species.

Each agent has a set of attribute declarations each of which specifies the identifier, the measurement unit and optionally the initial value of the attribute allocated in the persistent heap memory. An interaction among agents is modeled as an Action which consists of a set of attribute definitions, each of which modifies the next value of the attribute of an animat that participates in the interaction. Local variables are defined in the utility definitions so that right-hand expressions in attribute declarations and attribute definitions are concisely presented. A task definition binds an action to an agent so that each individual of the agent will do the action at every time step in the simulation. Fig. 4 shows a screenshot of RE:MOBIDYC running "eggs and grasshoppers", a simple model to explain the basic features of RE:MOBIDYC. The space is divided into rectangular patches, visualized as green rectangles in the figure, each of which has grass on it. A grasshopper, rendered as yellow dots in the figure, moves to the cell with the richest grass and eats it. Eating grass reduces the grass in the patch. The grasshopper also stores energy from food and metabolism reduces the energy at a certain rate. If the energy is below a threshold, the grasshopper starves to death. The grasshopper spawns eggs when it gets matured. An egg, rendered as cyan dots in the figure, does not do anything until it eventually hatches after a certain duration, and becomes a grasshopper. A chart of the population of eggs by time is displayed to the right. Details of these language constructs are explained later.

Agents and Attributes

An agent has a set of attributes, each of which consists of an identifier, a measurement unit, and an optional initial value. The measurement unit is used for type checking to be described in Section 2.5 and also to display numbers in visualization such as tables and charts. An attribute is a variable that stores a floating point number. All numbers in attributes and expressions of RE:MOBIDYC are in the SI unit. Stages implicitly have the

Actions and Tasks

Actions are core constructs of a model that represent interactions among agents as modifications to their attribute variables. RE:MOBIDYC employs discrete-event simulation with synchronous updates on memory, which holds all modifications to attributes during the computation at a time step.

To implement the synchronous updating memory, RE:MOBIDYC allocates three memory slots for an attribute: the value slot, the next slot, and the delta slot.

-The value slot is for the read access.

-The next slot and the next-delta slot are for the write access.

The interpreter can overwrite the next slot with a new value of the attribute for the next time step. The value will not be read until the next time step. The delta slot accumulates the increments/decrements to the attribute. The increments/decrements to an attribute across different actions will not affect the attribute until the next time step but are accumulated in the delta slot. At the end of the time step, the value slot is updated with the sum of the next slot and the delta slot. The details of the synchronous updating memory are explained in Section 2.6.

The synchronous updating memory was chosen due to DP5: The system should record all attribute variables of all agents at all time steps. The record of attribute variables at every time step carries all information about the simulation because the values of the attribute variables can change only at the transitions between time steps. Also, the synchronous updating semantics makes the semantics of actions closer to definitions of numeric sequence in the form of recurrence relation because neither the execution order of actions nor the order of agents affects the result of the simulation. All changes are accumulated and reflected regardless of the order of execution. Fig. 6. An example definition of actions in RE:MOBIDYC Fig. 6 shows the definitions of two actions, namely age and move in the RE:MOBIDYC modeling language. The age action has one attribute definition to add ∆time, the simulation time step defined as a simulation setting, to the age attribute of the agent that performs the action. Please note that which agent will perform this action is not specified yet. An agent and an action are bound by a task definition, which is described later in this section.

The move action modifies the attributes x and y of the performing agent using two utility variables theta and r defined below the where clause. A utility variable is a kind of temporary variable scoped within the action. Identifiers led by the prefix, such as the heading and the speed, are placeholders which will be replaced with concrete expressions in a task definition. Placeholder allows an action to have a generic parameter whose concrete argument may vary by the performer agent. Above the where clause, two attribute definitions on the x and y attributes are placed. An attribute definition with the d/dt decorator is equivalent to the attribute definition with ∆ operator and the righthand side multiplied by the simulation time step ∆time. For example, my d/dt x ′ = cos(theta)*r is equivalent to my ∆ x ′ = cos(theta)*r*∆time.

Adult move

where the speed -> uniform 0 [km/day] to 0.5 [km/day] the heading -> direction neighbor's grass. As stated in DP1: The language should be declarative and should not impose imperative programming, the action definition is in a declarative style. Assignments are listed at the top level of an action definition, and the right-hand sides are expressions which do not contain assignments. Built-in functions except random number generators in uniform, normal, gamma and log-logistic distributions are referentially transparent, and the interpreter manages internal states of random number generators to ensure reproducibility. Expressions such as arithmetics and built-in functions trivially correspond to their counterparts in mathematics. All values are floating point numbers and neither booleans nor agents are the first-class objects. No loop can appear in expressions including finding the local patch or nearby agents so that an execution of a simulation should halt or abort in a finite time. Finding a peer for interaction is done by the interpreter.

Formal Semantics of the Language

Although the language is intended to be easy to learn without prerequisite programming skills, its semantics should be defined without ambiguity as a tool for scientific research. For example, the internal state of the random number generator depends on the number of random numbers generated so far even when the same seed is specified. A precise process of execution must be specified to clarify, for example, when the right-hand side of a utility definition is evaluated and how many times. § The main objectives of defining the formal semantics of RE:MOBIDYC are not in mathematical proof of certain properties of the language, but to provide a clear reference of the language for understanding models and for ensuring compatibility of ported interpreters in future.

Execution semantics. The definitions of major operations related to evaluating expressions and attribute definitions are shown in Fig. The reference to a utility variable is defined in three steps: (1) try to read first and return if successful, (2) evaluate the right-hand side of the utility definition, and (3) store the result and return it. Thus, utility variables are evaluated on demand and written once for each evaluation of the action. The reference to an attribute variable defined by the readVariable operation states that the interpreter is also responsible for resolving the address of the attribute variable of an agent. It is also clear that the values of the utility variable are managed by the Interpreter module while the attribute variables are allocated in the Memory module.

The definitions of the writeVariable and writeDeltaVariable operations define the write access to the next slot and the delta slot accordingly, and the interpreter resolves the address of the specified attribute of the agent. The definition of the evalAttribut-eDefinition operation specifies the mapping between the decorators and memory's write-access API.

Type System

The modeling language of RE:MOBIDYC has a unique type system based on measurement units. All attribute variables, utility variables, and expressions in RE:MOBIDYC are floating point numbers with measurement units. All values are computed in SI units, and a pair of types are compatible when their measurement units have the same dimension. For example, an expression 10

[km] / 3 [h] is typed [km/h] with dimension [m/s]. 10 [km] + 3 [h]
is a type error because the + operator requires the both arguments in compatible types and [km] and [h] are not compatible. Two kinds of type casting expressions are provided; the en-unit conversion to attach a measurement unit to a non-dimensional number typed [], and the de-unit conversion to detach the measurement unit to generate a non-dimensional number. These type castings are useful when dealing with expressions with exponentials and logarithms. § Fig. 10 shows a snippet from the definition of measurement units in VDM-SL. The Unit type has two fields: the dimension field which has a sequence of SI base units and their orders, and the scale field for unit conversions in the type casting expressions and literal values with non-SI units. For example, the unit of speed [km/h] is represented as mk Unit([mk (¡m¿, 1), mk (¡s¿, -1)], 0.27777...). Although the temperature unit ¡degreeC¿ is not an SI base unit, RE:MOBIDYC handles it as if it were an SI base unit because the Celsius temperature is widely used in math models of Biology, e.g. degree day. The same applies to the Fahrenheit temperature.

Memory

As explained in Section 2.3, RE:MOBIDYC employs synchronous updates on memory. All modifications to attribute variables are delayed until the end of the time step. The values of all attributes are recorded to storage as required by DP5: the system should record all attribute variables of all agents at all time steps. Fig. 11 shows the specification of memory access in VDM-SL. The memory holds three mappings from Address to real as the memory's internal state. The state variables vals, next and delta hold the value slots of values, next and delta accordingly. The three operations read, write and writeDelta define the three kinds of access to the memory. Because operations are not first-class objects in VDM-SL, callers to the write and writeDelta operations can be statically analyzed to ensure the evaluation of expressions does not reach the write and writeDelta operations.

The values of all attributes are stored into storage. The store operation appends the sum of the next slot and the delta slot into the state variable valuesStorage typed as a sequence of real numbers. The load operation initializes the values slots and the next slots with the stored values, and sets the delta slots to zero. The store and load operations are called at transitions of simulation time steps to synchronize the three slots and the storage. These two operations abstract the implementation of the storage valuesStorage. The load operation takes the time step as the argument, which allows the simulation not only to proceed forward but also to be unwound to a point in the past to replay the simulation. In Pharo, the Observatory UI shown in Fig. 4 has a slider to control the simulation time step back and forth.

The formal specification of the memory brings the significant benefit of enabling multiple storage back-ends. In Pharo, two kinds of storage are implemented. One is onmemory storage which simply stores the values as an ordered collection object which runs fast but has the limitation of capacity. Small models with short simulation time run efficiently on the on-memory storage. Another is file-based storage which dumps the values into CSV files. The file-based storage uses less memory regardless of the number of time steps in the simulation, at the cost of the reading and writing files. It is also possible to implement a storage back-end on RDBMS shared by multiple users. In Pharo, an abstract class for storage defines the public API of storage classes. The formal specification in VDM-SL adds the semantic requirements of the API so that the user can safely choose any concrete storage.

Development Process

The development of RE:MOBIDYC is hosted on the github organization 1 Table 1 shows the progress of the development in sizes of implementation and specification. The Pharo LOC (all) column shows the total number of lines of source code stored in the repository, including GUIs, parsers and type checkers. The Pharo LOC (interp.) column shows the number of lines of code for interpretation, i.e. AST, evaluation and memory model. The LOC column shows the number of lines of the VDM specification for the corresponding parts.

By reading the time factors, the specification went far quicker than the implementation. Implementation in Pharo started in Oct 2019 and is still ongoing. The specification in VDM-SL started in Aug 2022, about 3 years after the start of the implementation by the same engineer who implemented it in Pharo. The specification was developed on ViennaTalk2 [START_REF] Oda | A formal modeling tool for exploratory modeling in software development[END_REF] and was also refined on the Overture VSCode plugin3 [START_REF] Rask | Visual Studio Code VDM Support[END_REF][START_REF] Rask | Advanced vdm support in visual studio code[END_REF]. The implementation for interpretation gradually increased throughout the development time and the specification caught up in four months. Please note that this should not be taken as the difference in productivity between Pharo and VDM. The difference reflects the cost of exploration to discover the language features validated by the domain experts. Building GUIs, designing concrete syntax, writing parsers, implementing various visualizations, creating type-checking algorithms, and communicating with domain experts are involved in the exploratory process.

The LOCs also indicate that the code in Pharo is about 10 times larger than its counterpart in VDM-SL. This also does not mean that the VDM is 10 times more productive than Pharo. Both Pharo and VDM provide high-level functions to manipulate abstract concepts such as finite sets and mappings. One source of the difference is the redundancy of Pharo's file format. Editing source files is not a typical way of programming in Pharo. Pharo provides powerful programming UIs that the programmer can interactively write code using automated tools. Accessor methods to read and write instance variables can be automatically generated by the tool, which takes a significant amount of lines when stored in a file.

Discussion

Successful cases of formal methods including VDM have shown that formal specification benefits the implementation phase in time, cost and quality [START_REF] Fitzgerald | Balancing Insight and Effort: the Industrial Uptake of Formal Methods[END_REF]. The development of RE:MOBIDYC went in the reverse order of the specification and its implementation. The specification of RE:MOBIDYC plays two roles in the development: an intermediate product as input to the implementation, and the specification itself is a part of the final product. The language is designed as a tool for scientific research and therefore its semantics should be rigorously defined and available to the open public.

Writing the specification from implementation went smoothly despite the difference in paradigms between Pharo and VDM-SL. Pharo is a dynamically-typed objectoriented language while VDM-SL is modularized definitions of types, values, functions, states, and operations without classes. There were minor mismatches in the way of the presentation of concepts between Pharo and VDM-SL. One is kind-of relations presented in a class hierarchy in Pharo. In VDM, they are presented as subtypes using union types. For example, an agent is either the world, a patch or a stage in RE:MOBIDYC. In Pharo, the classes for world definition, patch definition and stage definition are subclasses of the agent definition class. In VDM-SL, the AgentDefinition type is the union of WorldDefinition, PatchDefinition and AnimatDefinition. These subtype relations implemented in the class hierarchy are naturally rewritten as union types in VDM-SL.

An apparent difference in the presentation of implementation and specification is in how functions on AST nodes are defined. Although both Pharo and VDM-SL provide high-level functionalities such as sets and mappings, the specification in VDM-SL tends to be more compact than the source code in Pharo. The Pharo class for the agent definition node has 24 methods and its subclass for stage definition has 15 methods while the AST module in VDM-SL has only one function related to the agent definition, namely sizeOfAgent. Fields of a record value can be accessed by default as declared in the record type definition. In object-oriented programming, those accessor methods are considered good practice for specialization by inheritance, and Pharo's programming tools provide good UIs to operate over overridden small methods with less burden. Besides accessor methods, Pharo's flexible object system allows the programmer to define control structures as methods. The attributeDeclarationsDo: method of the agent definition class iterates over the attribute declarations to evaluate the closure. In the VDM specification, those enumerations are done by the language, i.e. the sequence-binds and for-in-do statements.

The cost of the specification phase has been a small fraction in the development of RE:MOBIDYC. Case studies of lightweight formal methods indicate that the formal specification improves the quality and productivity of the implementation. The cost of specification in the RE:MOBIDYC was insignificant when the explorative tasks were done in the preceding implementation phase.

Concluding Remarks

This paper reported the development of RE:MOBIDYC as a case of the implementationfirst approach of formal specification. The development time and amount of source text were significantly smaller than those of implementation. In successful cases of formal specification by conventional specification-first approach, specification took longer time than implementation. It is highly probable that the source of the cost of the specification case is more in the exploratory process than in presenting in formal specification lan-guages. The exploration to understand the problem domain and to communicate with domain experts is required in the development of novel software. The developers need to pay the cost of exploration regardless of which language to use in the exploration, a specification language or a programming language. Formal specification is applicable in either case. The authors consider that the case of RE:MOBIDYC introduced in this paper mentions that the implementation-first approach with an agile programming language can be a good choice of lightweight formal methods. Further study is needed to understand the effect of formal specification applied in the implementation-first approach.

Fig. 1 .Fig. 2 .

 12 Fig. 1. Screenshot of RE:MOBIDYC's GUI-based modeler

Fig. 3 .

 3 Fig. 3. Class diagram of re:mobidyc's modeling language AST

Fig. 4 .

 4 Fig. 4. Screenshot of re:mobidyc's Observatory

x

  and y attributes in m to hold the position of the agent. World represents the global environment and Patch represents a local environment of a square region of the space. Adult is Grasshopper with age [day]. Egg is Grasshopper with age [day] = 0 [day].

Fig. 5 .

 5 Fig. 5. Example definitions of two stages in RE:MOBIDYC

  to age is my ∆ age' = ∆ time. to move is my d/dt x' = cos(theta) * r my d/dt y' = sin(theta) * r where theta = the heading r = the speed.

Fig. 7 .

 7 Fig. 7. An example definition of a task in RE:MOBIDYC

Fig. 8 .

 8 Fig. 8. AST definition of actions in VDM-SL

typesFig. 10 .

 10 Fig. 10. The definition of measurement units in VDM-SL

  [START_REF] Oda | re: Mobidyc-reconstructing modeling based on individual for the dynamics of community[END_REF]. RE:MOBIDYC provides expressions such as variable references, literals, built-in functions, arithmetic operators and so on. The definition body of the evalExpression operation is a huge cases statement that defines how to evaluate each kind of expression. The semantics of variables with regard to read and write access is a core feature of RE:MOBIDYC. §

	evalExpression : AST'Expression ==> real
	evalExpression(expr) ==
	cases expr:
		mk_AST'UtilityVariable(identifier) ->
		let val = Interpreter'readUtility(identifier)
		in
		(if val <> nil then return val;
		let newval = evalExpression(
		Interpreter'getUtilityDefinition(identifier))
		in
		(Interpreter'writeUtility(identifier, newval);
		return newval)),
		mk_AST'AttributeVariable(agent, identifier) ->
		return Memory'read(
		Interpreter'getAttributeAddress(agent, identifier)),
		...
	end;
	readVariable : [AST'Identifier] * AST'Identifier ==> real
	readVariable(agent, identifier) ==
	return Memory'read(
		Interpreter'getAttributeAddress(agent, identifier));
	evalAttributeDefinition : AST'AttributeDefinition ==> ()
	evalAttributeDefinition(attributeDefinition) ==
	let
		value = evalExpression(attributeDefinition.expression),
		agent = attributeDefinition.variable.agent,
		identifier = attributeDefinition.variable.identifier
	in
		cases attributeDefinition.decorator:
		<assign> -> writeVariable(agent, identifier, value),
		<delta> -> writeDeltaVariable(agent, identifier, value),
		<differential> ->
		writeDeltaVariable(agent,identifier,value * deltaTime())
		end;
	writeVariable:[AST'Identifier] * AST'Identifier * real==>()
	writeVariable(agent, identifier, data) ==
	Memory'write(
		Interpreter'getAttributeAddress(agent, identifier),
		data);
	writeDeltaVariable:[AST'Identifier] * AST'Identifier * real==>()
	writeDeltaVariable(agent, identifier, data) ==
	Memory'writeDelta(
		Interpreter'getAttributeAddress(agent, identifier),
	¦	data);	¥
		Fig. 9. Semantics of variable references in VDM-SL

Table 1 .

 1 . Pharo source code and VDM-SL specification are together in the same repository. § Source size during development time

	types
		Address = nat1;
	state Memory of
		vals : map Address to real
		next : map Address to real
		delta : map Address to real
		...
		valuesStorage : seq of (map Address to real)
		animatsStorage : seq of (map Address to (AST'Identifier * nat1))
		ticks : nat
	init s == ...
	end
	operations
		pure read : Address ==> real
		read(address) ==
		if address in set dom vals
		then return vals(address)
		else exit ADDRESS_ERROR;
		write : Address * real ==> ()
		write(address, data) == next(address) := data;
		writeDelta : Address * real ==> ()
		writeDelta(address, data) ==
		if address in set dom delta
		then delta(address) := delta(address) + data
		else exit ADDRESS_ERROR;
		store : () ==> ()
		store() ==
		(valuesStorage := valuesStorage
		ˆ[{a|->next(a)+(if a in set dom delta then delta(a) else 0)
		| a in set dom next \ deads}];
		...)
		pre ticks = len valuesStorage and ticks = len animatsStorage;
		load : nat1 ==> ()
		load(t) ==
		(vals := valuesStorage(t);
		...
		next := vals;
		delta := {a |-> 0 | a in set dom vals};
		...
		ticks := t)
	¦	pre t <= len valuesStorage and t <= len animatsStorage;	¥
		Fig. 11. The definition of read and write access to the memory in VDM-SL

https://github.com/ReMobidyc/

https://github.com/tomooda/ViennaTalk

https://github.com/overturetool/vdm-vscode

Acknowledgments

The authors thank the Pharo community for technically supporting the implementation platform and the anonymous reviewers for their valuable comments and suggestions.


Mourad Korichi
email: m.korichi@arn.dz

Vincent Gerbaud
email: vincent.gerbaud@ensiacet.fr

Thierry Talou

Christine Raynaud

Pascal Floquet

Relation Structure moléculaire -Odeur Utilisation des Réseaux de Neurones pour l'estimation de l'Odeur Balsamique

Keywords: Molecular graph, Group contribution, Property prediction, CAMD

are key issues for the synthesis of new odorant molecules. But, this relation is hard to model, due to limited understanding of olfaction phenomena and the subjectivity of odor quantity and quality as stated in Rossitier's review (1996). Many molecular descriptors are used to correlate molecule's odor, but no universal rules emerge in this field. In this paper, we focus on the use of molecular descriptors as an alternative approach in the prediction of odors, by the mean of regression techniques. Principal Component Analysis (PCA) and Stepwise Collinearity Diagnosis (SCD) techniques are used to reduce the dimensionality of data, by the identification of significant molecular descriptors. Then, the chosen molecular descriptors are used with a neural networks algorithm to correlate the structure to molecular odor quality. The results are validated on balsamic flavor..

INTRODUCTION

Odorant compounds are found in a wide variety of products ranging from foods, perfumes, health care products and medicines. Either combined or alone, flavor and fragrance compounds are used to induce consumers to associate favorable impressions with a given product. In some cases, products have one predominant component which provides the characteristic odor. However, in most cases, products containing odors include a complex mixture of fragrant compounds. Some of them are classified within REACH, a European Community document, regulating the use of chemicals in terms of environment and toxicity. Structure -Odor relationships (SOR) are very important for the synthesis of new odorant molecules. This relation is difficult to model due to the subjectivity of the odor quantity and quality. Olfaction phenomenon is not yet completely understood and odor measurements are often inaccurate [START_REF] Amboni | [END_REF]. Research has been oriented to the use of structural, topological, geometrical, electronic, and physicochemical parameters as descriptors, to generate odor predictive equations. Therefore, a number of computational techniques have been used successfully. Artificial Neural Networks (ANN's) are one of these promising techniques readily suited for the assessment of poorly understood properties like odor. In this paper, we aim to use molecular descriptors as an alternative approach in the prediction of molecule's odor by the mean of regression techniques. Principal Component Analysis (PCA) and Pairwise Collinearity Diagnosis techniques are used to reduce the dimensionality of data, by the identification of significant molecular descriptors. SIMO 2006-systèmes d'information, modélisation, optimisation et commande en Génie des Procédés Le virtuel dans la réalité quotidienne. 11-12 octobre 2006 -Toulouse (France) Then, the chosen molecular descriptors are used with a neural networks algorithm to correlate the structure to molecular odor quality. Figure 1 summarizes the methodology.

MOLECULAR DESCRIPTOR SELECTION

Molecular descriptors accounts for a particular aspect of the molecule structure. As examples, simply count of atoms, functional groups and characteristic fragments are some of the constitutional descriptors family of the studied structure. Topological descriptors are related to the two-dimensional representation of the molecular structure. Molecular descriptors are the most significant common features of molecular structure that can be used to develop Structure -property relationships. In our case, the property is the odor of a molecule. Our input data set contains 121 molecules of balsamic odor splited in 5 sub-notes of typical odors (see Table 1): anise, balsam, honey, vanilla and sweet (Aldrich Flavors and Fragrances catalog, 2005). The dragon software (TALETE, 2005) is used to calculate up to 582 molecular descriptors of the input data set. According to figure 1, two cases are explored, first, 34 simple descriptors (molecular weight, aromatic ratio, number of benzene-like rings, connectivity indices, Kier symmetry index and n-path Kier alpha-modified shape index) used in the different relations described in Rossitier's review on structure -odor works since 1930 (1996) are calculated. In the second case, 582 molecular descriptors are considered: constitutional descriptors, topological indices, walk and path counts, connectivity and information indices, 2D autocorrelations, edge adjacency indices, burden eigenvalues and topological charge indices. All descriptors are calculated from the 2D molecular representation.

Complete Correlation Analysis

The complete correlation analysis is used to select a subset of linearly independent descriptors. Descriptor dependency is evaluated using the Dragon software by setting a predefined value Rmax (In this work, Rmax = 0.97) below which descriptors are considered linearly independent.

Principal component analysis

Principal component analysis is one of the oldest, but still most widely used techniques of multivariate analysis. The basic idea of the method is to try to describe the variation of the variables in a set of multivariate data, as parsimoniously as possible using a set of uncorrelated variables, each of which is a particular linear combination of those in the original data. This enables us to reduce the molecular descriptors dimensionality, by the identification of the principal components that can be used in the structure -odor relationship. All eigenvalues greater than 1 are retained to describe the principal axes.

In the first case, four principal components are kept to describe the 16 molecular descriptors, widely used in the correlation of the structure -odor. In the second case, ten principal components are retained to represent the 140 molecular descriptors.

ARTIFICIAL NEURAL NETWORKS (ANN) APPROACH

The ANN [START_REF] Dreyfus | Réseaux de neurones :: méthodologie et applications[END_REF] trained by back-propagation (BP) network algorithm has a two layers architecture: the first layer is called the hidden layer. The number of hidden neuron is a variable X between 7 and 9. The output layer consists of one neuron, namely the odor quality. The network configuration is m-X-1, where m represents the number of principal components encapsulating the maximum of information of the linearly independent molecular descriptors ( § 2.2). The ANN has a feed forward layered structure with connections allowed only between adjacent layers. The balsamic odor sub-notes as output, are represented by arbitrary continuous codification described in table 1. Input and output data are normalized, and hyperbolic tangent sigmoid transfer function is used in the hidden layer. The output layer is a linear function. In this work, the training and the validation sets are generated randomly, corresponding respectively to 70% and 30% of the input data set of 121 molecules. After several training sessions, an optimal number of hidden neurons X equal 8 and 7 is retained for case one and two respectively. The network is trained for 500 epochs with a gradient algorithm. The performance goal is 0.001.

DISCRIMINANT ANALYSIS

Discriminant analysis is an analytical technique, whereby a multivariate data set containing m variables is separated into a number (k) of pre-defined groups, using discriminant functions (Z) which are linear combinations of the variables. Two cases are studied to discriminate the molecules into different odors based on the results of PCA described on the paragraph ( §2.2).

Discriminant Analysis based on the first PCA study (four principal components)

In the first case there are four principal components. Results are presented in the table 3 with an overall 69.4% of the molecules in the data set, are well classified. The molecules of vanilla odor have the highest correctly classification per cent.

RESULTS AND DISCUSSIONS Artificial Neural Networks Approach

It is well-known that ANN performance depends on many variables, as the number of hidden neurons, the degree of homology between the training and the validation sets and the input variables (Principal components in this case). In figure 2, results are represented as the variation of the odor quality versus the molecule identification code, (a) for the first case and (b) for the second case. In the first case (a), the ANN does not converge as shown by the similarity of the response for all molecules despite their initial differences. In the second case (b), the training set is well represented, but almost all the validation set is not. This clearly shows the non predictive capacity of the ANN approach. Kovatcheva et al. (2004) on a kNN approach for modeling structure -ambergris odor relationship suggest to use division procedures based on sphere-exclusion algorithms and demonstrate a predictive capacity. But the ambergris odor is due to well known chemical structures, unlike the balsamic odor where molecule structure is more heterogeneous with several odor sub-notes. Also, Chastrette et al., (1995Chastrette et al., ( & 1996)), Cherqaoui et al. (1998) and [START_REF] Zakarya | [END_REF] do not consider sub-notes, only, requesting a discrete response. Discriminant Analysis Approach 69.4% and 83.4% of molecules are well discriminated in the two cases respectively, especially anise and vanilla molecules groups. This is better than the ANN approach. Case 2 has more odor discriminant, because it incorporates more numerous and diverse molecular descriptors. Among the molecules that are not discriminated, the two molecules from anise, classified in the vanilla group bear similar molecular structure with vanilla type molecules, which have three oxygen atoms, high Kier symmetry index and n-path Kier alpha-modified shape index. For case 2, in balsam and honey subnote odors, the molecule wrongly classified is considered differently depending on the referential nomenclature (we used Aldrich's) that both belong to balsamic and/or rose main odors. In the group of vanilla, one molecule is discriminated as balsam sub-note. From the referential nomenclature, we can say that the molecule has different odor types. In the sweet sub-note, fourteen molecules are distributed into other sub-notes. The low discrimination of the sweet odor may be attributed to the subjectivity of this sub-note, unlike vanilla or anise. Indeed, sweet is not considered as a typical odor type in the reputed referential chart "the field of odors" of [START_REF] Jaubert | [END_REF].

CONCLUSION AND PERSPECTIVES

In this work we present different ways to estimate and discriminate odors of molecules, based on molecular descriptors using multidimensional data analysis, and neural network applied to balsamic odors. The multidimensional data analysis is a powerful tool to reduce data sets and encapsulate the maximum of molecule's structure information. Discriminant analysis results using only 2D molecular representation are encouraging. Further work using 3D representation molecular descriptors may improve the results. The neural network satisfactorily correlates the molecules with their assigned odor, based on sufficiently numerous and diverse molecular descriptors. But it is unable to predict balsamic odor and its sub-notes. Compared with literature, successful results in ANN approach are due to the well known families of odor. The heterogeneous nature of the molecules assigned to balsamic odor and the absence of evident structure -odor relationship, forces us to request a continuous discrimination between sub-notes.

Figure 2 .

 2 Figure 2. Reference odor (Aldrich, 2005) and calculated odor versus molecular identification.

Table 1 .

 1 Input data set of molecular structure

	Odor type	Number of compounds	Arbitrary continuous Odor codification	Arbitrary discontinuous Odor codification
	Anise	10	0 to 0.15	0.15
	Balsam	18	0.25 to 0.35	0.35
	Honey	21	0.45 to 0.55	0.55
	Vanilla	15	0.60 to 0.75	0.75
	Sweet	58	0.85 to 0.95	0.95

Molecular Descriptors Selection 16 linearly independent descriptors 140 linearly independent descriptors 4 Principal components 10 Principal components 28 Molecular Descriptors:

  Constitutional, topological and connectivity. Mw, Aromaticity, nBz, nR5, nR6, SiK, XiA,

	582 Molecular Descriptors:
	Constitutional, topological, walk and path
	counts, connectivity , information, 2D
	autocorrelations, edge adjacency, burden
	eigenvalues and topological charge.

Complete Correlation Analysis Principal Component Analysis Discriminant Analysis Neural Network Figure

	SIMO 2006 -systèmes d'information, modélisation, optimisation et commande en Génie des Procédés
	Le virtuel dans la réalité quotidienne.
	11-12 octobre 2006 -Toulouse (France)
	Classification & regression

1. Schematic representation of methodology on structure -odor relationships.

Table 3 .

 3 Discriminant analysis based on the first PCA study.

	Groups	Anise	Balsam	Predicted groups Honey	Vanilla	Sweet	molecules	Correctly classified
	Anise	8	0	0	2	0	10	0.800
	Balsam	1	14	1	1	1	18	0.778
	Honey	0	3	15	0	3	21	0.714
	Vanilla	0	2	0	12	0	14	0.857
	Sweet	3	8	8	4	35	58	0.603

Discriminant Analysis based on the second PCA study (ten principal components) In

	SIMO 2006 -systèmes d'information, modélisation, optimisation et commande en Génie des Procédés
	Le virtuel dans la réalité quotidienne.
	11-12 octobre 2006 -Toulouse (France)

the second case, there are ten principal components. 83.4% of 121 molecules in the data set are well classified, with the honey molecules having the highest classification, and the sweet molecules having the lowest, like in the first case.

Table 4 .

 4 Discriminant analysis based on the second PCA study

	Groups	Anise	Balsam	Predicted groups Honey	Vanilla	Sweet	molecules	Correctly classified
	Anise	8	0	0	2	0	10	0.800
	Balsam	0	17	0	0	1	18	0.944
	Honey	0	0	20	0	1	21	0.952
	Vanilla	0	1	0	13	0	14	0.929
	Sweet	3	2	5	4	44	58	0.759