Blandine Nouvel

Véronique Humbert

Evelyne Sinigaglia

PACTOLS the French terminological Repository for Archaeology

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.


Alexandra Halchin
email: alexandra.halchin@enseeiht.fr

Yamine Ait-Ameur
email: yamine@enseeiht.fr

Neeraj Kumar Singh
email: nsingh@enseeiht.fr

Abderrahmane Feliachi

Julien Ordioni

Certified Embedding of B Models in an Integrated Verification Framework

Keywords: Formal Semantics, B to HLL Translation Validation, Theorem Proving, Model Animation

To check the correctness of heterogeneous models of a complex critical system is challenging to meet the certification standard. Such guarantee can be provided by embedding the heterogeneous models into an integrated modelling framework. This work is proposed in the B-PERFect project of RATP (Parisian Public Transport Operator and Maintainer), it aims to apply formal verification using the PERF approach on the integrated safety-critical software related to railway domain expressed in a single modelling language: HLL. This paper presents a certified translation from B formal language to HLL. The proposed approach uses HOL as a unified logical framework to describe the formal semantics and to formalize the translation relation of both languages. The developed Isabelle/HOL models are proved in order to guarantee the correctness of our translation process. Moreover, we have also used weak-bisimulation relation to check the correctness of translation steps. The overall approach is illustrated through a case study issued from a railway software system: onboard localization function. Furthermore, it discusses the integrated verification at system level.

I. INTRODUCTION

Nowadays, it is well known that the development of complex industrial systems, involving both hardware and software components, is becoming a huge task requiring high quality development processes. Moreover, when these systems deal with critical application domains, like transportation and aerospace, energy, etc., these processes need to set up rigorous verification and validation procedures. Formal approaches have proved useful to define such rigorous procedures.

Furthermore, in a system engineering context, the development of a complex system is not handled by a unique developer. Several stakeholders are involved in the different development processes and may handle a component (part or a piece) of the system to be developed. Each of these development processes gathers several development activities and models shared and distributed among all the stakeholders. A consequence of the involvements of many actors in such developments is heterogeneity. Indeed, several modeling techniques, programming languages, design processes, validation and verification procedures, etc. may be set up by each stakeholder. Each stakeholder delivers the component (hardware or software) he/she is in charge of. Then, the main issue resided in the global verification and validation of the whole complex system. To solve this issue, one solution consists in imposing a standardized approach based on shared processes and languages. This approach is not realistic when the systems are too complex.

Our concern is the validation and verification of systems developed by various stakeholders who use their own modelling languages and development processes. We believe that black box validation and verification procedures can be set up. We show that formal modelling techniques provide a rigorous solution to allow integrated verification and validation activities.

Our work is inspired by railway transportation system development processes set up at RATP. For several years, RATP has been involved in the application of formal verification techniques to assess the safety level of railway systems which gave birth to a formal verification methodology called PERF (Proof Executed over a Retro engineered Formal model) [START_REF] Benaissa | The perf approach for formal verification[END_REF], designed to be applicable to any software system independently of their development processes and languages. The approach consists in diving all the produced component models in a single shared PERF pivot modelling language supporting formal verification. The PERF pivot language, HLL [START_REF] Ordioni | HLL v.2.7 Modelling Language Specification[END_REF], is a synchronous data-flow language, similar to Lustre [START_REF] Halbwachs | The synchronous data flow programming language lustre[END_REF], allowing to express, in the same formalism, the system behavior as well as safety requirements. This translation shall be sound and semantic preserving. Once this translation is achieved, it becomes possible to question the obtained shared models, for verification and validation purposes.

In this paper, we deal with the B method [START_REF]The B-book: assigning programs to meanings[END_REF]. The B-PERFect project was initiated in order to investigate the applicability of PERF on software systems developed using the B method [START_REF]The B-book: assigning programs to meanings[END_REF]. Software systems developed using B are valid by correct by construction with respect to safety requirements. The idea behind the B-PERFect project is not to replace the formal verification process of B but to propose a verification alternative to be used for an internal independent safety assessment. This will not question the proof process of B. However, it may eventually reveal any error in the initial formalization of safety requirements. The proposed method for safety-critical software verification is a bottom-up approach starting from the source code to the high level specification.

On these basis, in our approach, B models are automatically translated into HLL models. As this approach relies on a translator tool, a vital property is the semantic preservation and thus the certification of the translator.

In this paper, we address the problem of validating the translator by proving semantic equivalence between the source code and the target code. To prove the correctness of the program transformation, the formal semantics of each modelling language is expressed in Isabelle/HOL. Furthermore, a formal proof of semantic preservation (semantic equivalence) is carried out. It guarantees the equivalence between the B source language and the HLL target language. The overall approach is exemplified through a case study borrowed from the railway domain and supplied by RATP. The rest of the paper is organized as follows. Section II introduces the PERF approach and the case study illustrating our approach. An overview of our framework and basic concepts of B and HLL language are given in III. Section IV presents the B2HLL tool. The Isabelle/HOL formalization and the proof of the semantics equivalence is presented in Section V. In Section VI, the animation of the Isabelle/HOL formalization is described. Section VII discusses the related work and Section VIII gives some concluding remarks.

II. PERF: AN INTEGRATION VERIFICATION FRAMEWORK

RATP's engineering department relies on rigorous verification methodologies based on formal methods. The use of formal methods has been successfully applied for several RATP projects development, revealing safety critical bugs. RATP projects involve various subcontractors who use different development methods and languages. The resulting heterogeneity enforces RATP to master all subcontractor's methods and languages and to manage a complex assessment process. To deal with this complexity, a unified verification approach, offering an "ex post facto" proof, is applied to each supplied product independently of the subcontractor's development language or method.

A. The PERF Framework

The PERF verification process consists in translating the source code of the system under investigation into a formal HLL model. The safety properties, corresponding to the global requirements of RATP, are also expressed in HLL as proof obligations. The obtained model is completed (close loop modelling) with constraints or assumptions describing a model of the environment. Then, verification is performed on the obtained model. If the proof engine reveals counter-examples, the corresponding scenario is analyzed in order to understand the safety risk related to this property violation. A complete tool chain associated to PERF (translators, counter-example analyzers, SAT-based proof engines [START_REF] Prasad | A survey of recent advances in sat-based formal verification[END_REF]) is available.

PERF is actually applied in every project where translators are available. Programming and modelling languages like C, Ada or Scade are currently supported by PERF. It has been successfully set up to verify systems like Computer Based Interlockings, wayside and onboard equipments of CBTC (Communication Based Train Control) [START_REF] Feliachi | Formal verification of system-level safety properties on railway software[END_REF].

B. B-PERFect Motivation

In railway domain, due to the existing gap between highlevel system specification and low-level software implementation, the safety assurance is difficult to obtain. Moreover, gluing the safety risks expressed at the system level with the software components responsible for handling these risks is a hard task. The B method is proved useful to reduce this gap by defining a refinement chain moving from high level specifications to low level ones. But, independent assessment of safety-critical systems developed using the B method with respect to informal requirements can be complicated and might be intrusive in some situations. The detection of inconsistencies in invariants cannot be done automatically.

Even though the formal verification performed by the B proof engines can be trusted, the validation of the safety properties can only be performed by tedious and non efficient reviewing activities of code or specification. . To address the above constraints, the B-PERFect project provides an independent alternative for the verification of the safety properties on systems developed using the B method. According to the PERF approach, the B models are transformed into HLL models where the required safety requirements are added for checking the correctness of system behaviour. By doing so, one can prove additional system properties. The idea behind this is not to prove again the already proved properties on the supplied B models but to guarantee the safety properties which could not be expressed on the isolated B model due to the absence of its environment. This process is non intrusive and supports a verification of the integration of all system components.

C. Case study: Train localization in a CBTC system CBTC [7] is a complex system which uses bidirectional communication between onboard and wayside equipments in order to ensure a safe and high performance service. It is composed of different sub-systems that depend on each supplier's architecture, specification and development formalism. A CBTC system offers two main functions 1) localization (onboard), and 2) tracking of trains (wayside). Localization computes the topological position of trains while tracking uses Localization to build the cartography of the trains on the whole network.

In this case study, we are concerned with Train Reference-Point Localization TRPL function, a sub-function of the Localization. Given a topology of n line segments, a travelled distance estimation d and a train position p corresponding to a segment identifier, an abscissa and an orientation, the TRPL function computes the new train position p .

In order to reduce the complexity of the TRPL function, environment based assumptions are considered i.e. 1) a railway line is considered as a sequence (consecutive) of segments of equal length associated with an identifier 2) the train orientation is a one way and remains the same for all the segments. In an ideal world, the verification can be performed on the highlevel system requirements and their low-level implementation under the given safety properties. Unfortunately, this is not possible because either the developed model is too complex or the given safety properties do not address directly the developed high-level requirements.

The following requirements are associated to TRPL. First unitary requirements (checked on the TRPL function in isolation) and second integration or system requirements, involving the environment assumptions, are presented.

1) Unitary requirements:

UnitReq1

The train reference point position p shall be computed according to the given orientation.

UnitReq2

The distance between the current reference point position p and the next reference point position p shall be equal to the travelled distance d.

UnitReq3

The train reference point position p shall not change when the new position goes beyond the known segments zone n.

2) Integration or system requirements: The system requirement on the TRPL function expresses that the reference point positions are computed on each consecutive segment crossed by a train. It entails checking that the next segment is not occupied. Safety specifications can have different levels of refinement and not all of the requirements are directly encoded in the B model as invariant or by implementation. For the purpose of this paper, observe that this requirement is not defined in the B model, it is checked at the integrated HLL model level because it is defined over several models.

SystReq

The next reference point position shall be on the next segment (adjacent to the current segment position) in the given orientation

III. CERTIFIED EMBEDDING OF B MODELS

In the context of the B-PERFect project, as mentioned previously, our aim is to deploy the PERF approach for B models. We aim at developing a certified semantic preserving translator of B models to HLL. We prove that the translator B2HLL together with its implemented transformation rules defined in [START_REF] Halchin | Bperfect -applying the PERF approach to B based system developments[END_REF] is semantic preserving.

A. Our framework

Our approach is depicted in Fig. 1. It is based on a deep embedding using the Isabelle/HOL framework as a unified formal modelling framework. First, both B and HLL modelling language semantics are modelled in Isabelle/HOL. Then, an equivalence relation between these models is formalized. It is based on a bi-simulation relation (upper part of Fig. 1). An equivalence theorem is stated and proved (by a structural induction) once for all. Specific B and HLL models are checked to be equivalent as follows. Each B and HLL models are defined as instances of these semantic models (Instance of relation on Fig. 1). Then, the equivalence theorem associated to the defined equivalence is checked for these two instances. All the proof obligations are successfully discharged.

Discharging the proof obligations associated to the instantiation of the equivalence theorem (checking the theorem hypotheses) certifies that B and HLL models are equivalent according to the defined equivalence relation. The construction of proofs is mechanical. It is the responsibility of developer to discharge the verification condition in Isabelle/HOL using different tactics and to prove that the theorem hypotheses hold. Isabelle/HOL toolkit and its library of tactics are used for this purpose. Finally, an export tool (lower part of Fig. 1) produces Isabelle/HOL models for the specific input B models and HLL models produced by B2HLL tool.

B. HLL modelling language

HLL is a formal declarative and synchronous data flow language close to LUSTRE [START_REF] Halbwachs | The synchronous data flow programming language lustre[END_REF]. HLL models are seen as typed streams defined as compositions of either temporal or data operators. Temporal operators describe clock-dependent expressions while data operators, like arithmetic, logical or array operators, are used to manipulate streams values (being either integer or boolean values). The declarative nature of the language eases the definition of formal behavioural models as well as safety properties. A HLL project is organized in namespaces sections. Streams are declared in declarations blocks with type checking information, and their values are given in the definitions blocks. The proof obligations block contains a set of properties related to streams for requirement verification purpose. Constraints expressions are used to reduce the domain definition of unbound inputs streams.

C. The B Method

The B method [START_REF]The B-book: assigning programs to meanings[END_REF] handles complete critical-software development processes from specification to code using refinement. A B development process is layered. Each layer corresponds to an abstraction level and the refinement provides the relation between layers. B is based on first-order logic and set theory. Models are represented in B as machines. A machine contains state variables, instances of other machines, type invariants, an initialization clause and operations acting on the defined state variables. Generally, B project models represent a state transition system in which the initialization clause sets the initial values of variables and the operation clause specifies how variables are modified from one state to another. The invariant (first order logic expression) describes the safety properties of the model. Invariant preservation proof obligations are generated and need to be discharged in order to assert machine consistency. The highest level of abstraction is the specification, a representation of functional requirements and the lowest one corresponds to an implementation where only programming-like constructs are allowed [START_REF] Clearsy | Atelier b user manual version 4[END_REF].

D. Isabelle/HOL

In the style of LCF [START_REF] Gordon | Edinburgh LCF[END_REF], Isabelle/HOL is a generic interactive theorem prover for Higher-Order Logic (HOL) [START_REF] Nipkow | Isabelle/HOL: A Proof Assistant for Higher-order Logic[END_REF]. It is based on a meta logic used to encode object logics like First-Order Logic and Zermelo-Fraenkel set theory and offers a natural-deduction-style proof rules. The modelling part relies on functional programming languages. Basic type declaration is typedecl('t 1 , 't 2 , ...) T new , where 't i are possible type parameters and T new is a new defined type. Other type constructors are available: t i × t j for product and t i ⇒ t j for function maps. Moreover, it also supports condition, let and case expressions, which are basic constructs of the functional languages. Several powerful external provers are integrated in Isabelle/HOL.

IV. B2HLL: A TRANSLATOR FROM B TO HLL

In [START_REF] Halchin | Bperfect -applying the PERF approach to B based system developments[END_REF], we have described the general transformation principles from B to HLL, including the B2HLL tool we implemented. Below, we illustrate this transformation and show how a B model corresponding to the case study of section II-C, carrying the unitary requirements is translated to a HLL model.

A. From B to HLL 1

Due to the semantic mismatch, the transformation of B models to HLL models is not straightforward. On the B side, imperative style is used while data flow paradigm with single static assignment form (SSA) is used on the HLL side. B constants are directly translated into HLL constants and the typing invariants of B are equivalently translated to HLL datatypes. A particular issue in this transformation concerns B state variable evolutions and updates. A specific dataflow shall be defined on the HLL side to record the changes. B state variables become HLL data streams. Each B state variable updated in a B conditional statement becomes a HLL conditional expression that merges the information from different control flow branches associated to the evolution of the variable. Expressions, conditionals and loops are also translated in HLL. Regarding properties, HLL provides the same quantifiers as B language, the translation of B predicates and B expressions is almost straightforward. Finally, each B operation is translated to a HLL namespace as a sequence of assignments. More details on this transformation can be found in [START_REF] Halchin | Bperfect -applying the PERF approach to B based system developments[END_REF].

B. A B model for TRPL

Listing 1-2 shows the obtained implementation of the last level of a B refinement. The B model associated to the TRPL defines the context of the model by introducing constants for predefined limits (i.e. maximum number of segments, the length of a segment, maximal distance of displacement). 1 The complete B and HLL models are available at: http://yamine.perso.enseeiht.fr/TASE_Annex.pdf These constants are used to define a topolgy of the railway network in the T yp1, T yp2 and T yp3. The state variables are: v_segment-a new segment identifier; v_segment_bef ore -a previous segment identifier; v_absOnSegment -an abscissa on the current segment; v_absOnSegment_bef ore -a previous abscissa on the segment; and v_is_segment_found -to state if a new position is found in the limit of known zone of segments. They are typed in the Inv1, Inv2, Inv3 and Inv4.

Unitary requirements defined in section II-C are modelled in the invariant clause as safety properties (UnitReq1, UnitReq2 and UnitReq3).

Several operations are introduced, they modify the state variables. To illustrate our approach, only the implementation level of the findLoc procedure is presented. When the new position of a train remains in its bounds, the findLoc procedure changes the train reference point position based on a displacement i_dep, a previous segment i_seg and abscissa i_abs given as parameters. A while loop ensures that the segment identifier is increased when the train displacement is greater than the length of a segment. The loop invariant states that the input parameters respect their typing properties and the new train reference point is correctly computed by preserving the model invariants. The operation findLoc is triggered by the main program that models the current TRPL updates for a train displacement given by odometry devices. The developed B model is successfully proved using Atelier B [START_REF] Clearsy | Atelier b user manual version 4[END_REF] ensuring invariant preservation and thus fulfilling the unitary requirements.

C. A HLL model for TRPL

Starting from the B model described above, a HLL model is produced by the B2HLL tool according to the transformation principles defined in section IV-A. B state variables are represented as flows using cyclic definition in the HLL model. For each B implementation, the transformation process starts by producing corresponding HLL namespaces. Then, state variables flows are initialized starting from the B initialisation clause. The next values in the state variables flows are produced from the transformation of the B operations and the corresponding programming constructs. This behaviour is exemplified in listing 3. For example, the v_seg B state variable is updated with respect to the computed value in the B operation findLoc. The new computed values of the variable "v_seg_0" are used as inputs in the model "findLoc_0" to compute the next possible values of the variable v_seg. Note that each state variable named V arName is duplicated using an integer i suffix V arName_i to avoid side effects and to allow the HLL model to observe all the internal variables behaviours.

All the B constructs are transformed into HLL. Assignments become HLL assignments performed in sequence with a new integer suffix for each involved variables. Conditional expressions are transformed in two steps. First the then and else branches are translated, and then the conditional expression is built. B looping (while) construct is transformed into a recursive conditional statement. The B variant determines the number of iterations for termination.

Namespaces : " T r a i n P o s i t i o n i n g _ 0 " { . . . Types : i n t [ 1 , c_nb_segments ] Listing 3. HLL TRPL Properties Namespaces : " findLoc_0 "{ D e f i n i t i o n s : / / mapping i n p u t p a r a m e t e r s i_dep_0 := l_xDep_0 ; i _ a b s _ 0 := v_absOnSeg_0 ; i _ s e g _ 0 := v_seg_0 ; / / d i s t a n c e computation l_x_0 := i _ a b s _ 0 + i_dep_0 ; l _ s e g _ 0 := i _ s e g _ 0 ; / / Begin While I t e r 0 l_x_1 := l_x_0c _ s e g m e n t _ l e n g t h ; l _ s e g _ 1 := l _ s e g _ 0 + 1 ; l_x_2 := i f c _ s e g m e n t _ l e n g t h < l_x_0 & ( l _ s e g _ 0 < c_nb_segments ) t h e n l_x_1 e l s e l_x_0 ; l _ s e g _ 2 := i f c _ s e g m e n t _ l e n g t h < l_x_0 & ( l _ s e g _ 0 < c_nb_segments ) t h e n l _ s e g _ 1 e l s e l _ s e g _ 0 ; . . . / / End I t e r 0 v_absOnSegment_1 := l_x_20 ; / / IF cond v_segment_1 := l _ s e g _ 2 0 ; / / IF body v_segment_2 := i f ( v_isSegmentFound_1== t r u e )

t h e n v_segment_1 e l s e v_segment_0 ; v_absOnSegment_2 := i f ( v_isSegmentFound_1 == t r u e ) t h e n v_absOnSegment_1 e l s e v_absOnSegment_0 ; . . . } D e f i n i t i o n s : / / S t a t e v a r i a b l e s u p d a t e s v_segment_1 := : : " findLoc_0 " : : v_segment_2 ; v_isSegmentFound_1 := : : " findLoc_0 " : :

D. System analysis

Up to now, all the properties established in B are also the properties of the HLL model. One may ask what is the added value of such a transformation.

The interest of integrating the models in the HLL framework is double. First it allows to have a shared model obtained for various modelling languages and second it allows to check global properties at system level using a non intrusive approach (the source models are not modified). For example, the system requirement SystReq encoded in HLL (not expressed in the B model) as presented in listing 5 requires that, when a train moves, the next segment associated to the new train position is either the same one or the next one. The requirement does not allow trains to move forward to any segment. Only consecutive segment changes are allowed.

Proof O b l i g a t i o n s : / / SystReq v_seg = pre ( v_seg , 1 ) ∨ v_seg = pre ( v_seg , 1 ) + 1 ;

Listing 5. System level Requirement This requirement is not fulfilled by the produced HLL model shown above and the proof engine revealed a counter-example. The corresponding scenario was analyzed to understand the risk related to this property violation. This analysis revealed a possible environment restriction hypothesis related to the limitation of the maximum travelled distance (therefore of the speed, of the period of sensing position, etc.) in a cycle.

V. CERTIFIED TRANSLATION

This section addresses the last step of the formal verification and validation process we have set up when using the PERF framework. It consists in certifying the transformation process by formally guaranteeing semantic preservation after translation. We give the details of the Isabelle/HOL based certification process defined in section III-A.

Our goal is to show that the semantics of a source B model is preserved with the semantics of the translated HLL model. For this purpose, we define an equivalence relationship using a weak bi-simulation relationship relating B states and HLL flows. A deep embedding approach is defined. It consists in formalizing B, HLL and the equivalence relationship in Isabelle/HOL and prove that the transformation preserves equivalence. The proof is a structural induction on the constructs of the modelling language and on the transformation rules. Isabelle/HOL data-types and functions formalize all the concepts of both B and HLL. Below we give the main structure of this deep embedding.

A. Types and values

Isabelle/HOL data-types modelling features and constructs of B and HLL (states, flows, expressions, modelling statements) are defined. Variables names, variable values and an environment function associating variables to their values are introduced in Listing 6 where T val represents primitive types, varname defines a variable name with the associated type (powerset) and env is the environment function.

datatype Tval = Bool | I n t type_synonym varname = " name × Tval " type_synonym env = " varname ⇒ v a l " Listing 6. Environment function for variables

B. B Semantics in Isabelle/HOL

The semantics of B is described using a semantic function structurally defined on each B syntactic constructs.

1) B Syntax: Specific data-types for arithmetic expressions aexp, boolean expressions bexp and B statements instruction (a bloc of instructions for sequence, skip, assignment, and conditional) are defined in Listings 7, 8, and 9 respectively to model B abstract syntax. 3) The case of loops: The above defined semantic function does not handle the while loop statement. As mentioned in section IV-C the transformation tool translates such a loop to the recursive function b_while_to_if with conditional (see Listing 11). In this Listing, we observe that the function is called a nb number of times corresponding to the original B VARIANT value. It produces a sequence of if then else statements in a bloc Bl. In other words, each loop is unfolded recursively to a sequence of if then else statements.

fun b _ w h i l e _ t o _ i f : : " n a t ⇒ bexp ⇒ i n s t r u c t i o n ⇒ i n s t r u c t i o n " where " b _ w h i l e _ t o _ i f 0 _ _ = SKIP " | " b _ w h i l e _ t o _ i f ( Suc nb ) c i = Bl [ I f c i SKIP , ( b _ w h i l e _ t o _ i f nb c i ) ] "

Listing 11. A recursive function encoding while loops

The built-in fixpoint operator available in Isabelle/HOL defines the semantics of such recursive functions. Therefore, the conditional is enough to translate the whole B constructs of the IMPLEMENTATION level.

4) TRPL model of B in Isabelle/HOL:

The developed model of the selected case study is embedded (exported as instance) in Isabelle/HOL. All the state variables are flattened. All the TRPL operations are directly encoded in Isabelle/HOL applying the formalized B semantics.

C. HLL Semantics in Isabelle/HOL

As for B, the semantics of HLL in Isabelle/HOL is given. The HLL flows (streams) are defined as total functions mapping naturals on a polymorphic data-type in Listing 12. type_synonym ' a s t r e a m = " n a t ⇒ ' a " datatype v a l = B " bool s t r e a m " | I " i n t s t r e a m " Listing 12. Data type for HLL flows (streams) HLL variables are defined as (name×T val)×nat. In addition, each variable is identified using a unique natural number.

1) HLL Syntax: Similarly to B, specific data-types for arithmetic expressions aexp, boolean expressions bexp and statements instruction are defined. A specific expression is the conditional expression is added. Last, statements (bloc of assignements as instructions) are defined. Listings 13, 14, and 15 show these definitions in Isabelle/HOL. 2) HLL Semantics: The semantics of the HLL language imposes that the updating of the flows is performed in a synchronous manner i.e. the flows are modified simultaneously and there is no side effect. The function stream_comp (see Listing 16) has been defined in order to compose different stream values. This function is call by the semantic function interpreting the HLL statements. Like for B, the HLL semantics is given by semantic functions defined structurally on the corresponding syntactic constructs. The defined function meaning_exp ∈ exp → env → val interprets expressions while the meaning_instruction ∈ instruction → env → env function updates the environment of flows according to the semantics of the HLL statement (See Listings 17 and 18).

fun m e a n i n g _ i n s t r u c t i o n : : " i n s t r u c t i o n ⇒ env ⇒ env " where " m e a n i n g _ i n s t r u c t i o n ( Bl l i s t ) σ = ( c a s e l i s t of [ ] ⇒ σ | e#l ⇒ m e a n i n g _ i n s t r u c t i o n ( Bl l ) ( m e a n i n g _ i n s t r u c t i o n e σ ) ) " | " m e a n i n g _ i n s t r u c t i o n ( Assign vn exp ) σ = σ ( vn := meaning_exp exp σ ) " | " m e a n i n g _ i n s t r u c t i o n ( Assign ' vn exp1 exp2 ) σ = ( l e t v1 = meaning_exp exp1 σ i n l e t v2 = meaning_exp exp2 σ i n σ ( vn := stream_comp v1 v2 ) ) "

Listing 18. Semantics of HLL statements

3) TRPL model of HLL in Isabelle/HOL: Like for B, the HLL model of the selected case study, obtained by transformation, is embedded (exported as instance) in the Isabelle/HOL. All the state variables are flattened. Note that the HLL formalization in Isabelle/HOL does not take into account the notion of Namespaces. To address this issue the HLL variable names are prefixed with the name of the namespace where they are declared.

D. Certification of the translation

Once the B and HLL semantics are encoded in Isabelle/HOL, we have to formally define the transformation function and the equivalence theorem asserting semantic preservation. We describe the specification of the B2HLL translation [START_REF] Halchin | Bperfect -applying the PERF approach to B based system developments[END_REF] in Isabelle/HOL and then discuss the semantic preservation by defining an equivalence relationship.

1) The Transformation Function: This function is defined on the syntactic constructs identified for both B and HLL.

First, we address the mapping of B state variables to HLL flows (streams) which require a specific process. Each B variable identifier is mapped to a pair of HLL identifiers by M apping = Bvname → (Hllvname × Hllvname) where the first one is used for expression evaluation and the second one for mapping updates.

B Expressions and statements are transformed by T _exp ∈ Bexp → M apping → HLLexp and T ransf ormation ∈ Binstruction → M apping → (HLLinstruction × mapping) functions, respectively. For both expressions and statements, the defined M apping for variables is used to retrieve the HLL variable associated to each B variable. 2) The equivalence relationship: We define equivalence on state variables using an observational (bisimulation) relation [START_REF] Sangiorgi | On the bisimulation proof method[END_REF] between states on the B side and HLL flows on the other side. Listing 20 defines this relation for the case of integer and boolean types. It has to be defined for all other types.

d e f i n i t i o n meaning_equiv : : " b . env ⇒ mapping ⇒ h l l . env ⇒ bool " ( " _ ∼ = _ _ " ) where " b ∼ =m h ≡ ∀ v ∈ ( dom m) . c a s e v of ( vname , Tval . Bool ) ⇒ ( ( b v ) bool ( ( h o ( f s t o ( t h e o m) ) ) v ) ) | ( vname , T v a l . I n t ) ⇒ ( ( b v ) i n t ( ( h o ( f s t o ( t h e o m) ) ) v ) ) "
Listing 20. State equivalence Relation (bi-simulation)

This definition defines the initial property of the inductive proof process of semantic preservation.

3) Asserting the correctness of transformation: All the ingredients to write the equivalence theorem are available. Listing 21 describes the global equivalence theorem defining the semantic preservation property. Let CodeB and codeHLL be a B code and a HLL code, and σ B and σ HLL be two states for B and HLL respectively (lines 1 and 2 in Listing 21) such that σ B and σ HLL are equivalent by the meaning_equiv relation (line 5 in Listing 21). This theorem asserts under the assumption that the transformation of the codeB gives a codeHLL (Line 4 in Listing 21), the meaning_equiv relation holds on the semantics of the codeB and codeHLL in the states σ B and σ HLL , respectively (Line 10 in Listing 21).

theorem E q u i v a l e n c e : 1 . f i x e s codeB : : " b . i n s t r u c t i o n " and σ B : : " b . env " 2 . and codeHLL : : " h l l . i n s t r u c t i o n " and σ HLL : : " h l l . env " 3 . and n m : : mapping 4 . assumes * : " ( codeHLL , m) = T r a n s f o r m a t i o n codeB n " 5 . and # : "σ B ∼ =n σ HLL " 6 . and $ : " f i n i t e (dom n ) " 7 . and @ : " w e l l _ d e f i n e d codeB n " 8 . and ♣ : " w e l l _ d e f i n e d _ m a p p i n g n " 9 . and ~: " w e l l _ d e f i n e d _ s t a t e σ HLL " shows 1 0 . " ( b . m e a n i n g _ i n s t r u c t i o n codeB σ B ) ∼ = m ( h l l . m e a n i n g _ i n s t r u c t i o n codeHLL σ HLL ) "

Listing 21. Main Equivalence Theorem

4) Proving semantic preservation:

The proof of the equivalence theorem of Listing 21 is performed using the theorem prover of Isabelle/HOL. Most of the proofs are interactive (semi-automatic), they are completed through user interaction with the theorem prover of Isabelle/HOL.

A structural induction with case based reasoning (for each syntactic construct) have been set up. These cases have been decomposed into several lemmas which have been used for the proof of the main equivalence theorem. However, some complex transformation rules may require more elaborated proofs. For example, the semantic preservation proof for if conditional requires more than 300 lines of proof script and uses 25 lemmas to complete the proof.

In summary, the proof of the correctness of the transformation from B to HLL represents more than 5000 lines of proof scripts for discharging the proof obligations related to the transformation associated to the equivalence proofs.

VI. THE TRANSFORMATION AT WORK

The previous sections showed a complete transformation process together with a proof of equivalence. Theorem prover is a standard approach that can be used to prove the given properties in form of lemmas and theorems by checking every possible states of the system. Trying to prove an incorrect proposition may lead to dead-ends or considerable time loss. Therefore, the idea of debugging proofs by testing the conjunctures is helpful. Model animation is a powerful technique to perform such tests. We have used a model animator, available in the Isabelle/HOL tool, to validate our transformation on several examples, they helped to identify the right formlisation of definitions, lemmas and theorems.

Moreover, we have used model animation on the TRPL case study presented in section II-C for the models defined in sections IV-B and IV-C. By animating the main equivalence proof, we have shown that the output HLL model computed by the B2HLL tool is equivalent to the source B model, with respect to the defined transformation rules. In the process of safety assessment, the validation of the translator is an important step. Even though the B to HLL transformation is automatic, the model animation is interactive. This approach was applied to several case studies provided by RATP and the industrialization of the tool is ongoing.

VII. RELATED WORK

The formal validation and certification of translators has been studied by several authors. In general, the compiler is regarded as a black box and the semantic equivalence is established by performing proofs based on semantic relationships between source and target programs. Many contributions studied compiler certification for various language paradigms using different provers. [START_REF] Strecker | Formal verification of a java compiler in isabelle[END_REF] shows the formal verification of transformation of Java programs to Java byte code using Isabelle/HOL. [START_REF] Besnard | Automatic translation of c/c++ parallel code into synchronous formalism using an ssa intermediate form[END_REF] presents a formal approach for translating imperative code, such as C and C++, into the synchronous formalism Signal [START_REF] Gamati | Designing Embedded Systems with the SIGNAL Programming Language: Synchronous, Reactive Specification[END_REF]. In this work, model-checker is used to check the required properties. Pop et al. [START_REF] Pop | In and Out of SSA : a Denotational Specification[END_REF] present nonstandard denotational specification of the SSA form, including its conversion from imperative languages to SSA, and vice versa. A similar approach is presented in [START_REF] Blech | A formal correctness proof for code generation from ssa form in isabelle/hol[END_REF] for the SSA formalization. An automatic generation of correct program translation is described in [START_REF] Blech | A certifying code generation phase[END_REF]. The semantic equivalence of the source and the target code is showed using a simulation based proof. The CompCert compiler [START_REF] Leroy | Formal verification of a realistic compiler[END_REF] is a formally certified translator using Coq proof assistant [START_REF] Bertot | Interactive theorem proving and program development[END_REF] to generate the assembly code from the C language. The generated code is obtained directly from the theorem prover. Formal compiler verification is presented in [START_REF] Bourke | A formally verified compiler for lustre[END_REF], [START_REF] Biernacki | Clock-directed modular code generation from synchronous block diagrams[END_REF] using LUSTRE. [START_REF] Ryabtsev | Translation validation: From simulink to c[END_REF], [START_REF] Pnueli | Translation validation: From signal to c[END_REF] present synchronous versus sequential code validation based on the proof strategy. In our work, we have adopted the similar approach to establish an equivalence relation between the semantic states of the two models that can be preserved by the execution steps. Compared to the other approaches, ours is open and does not rely on any specific modelling language.

VIII. CONCLUSION & FUTURE WORK

This paper presented a complete formal verification process for checking requirements at both functional and system level on B models. The approach consists in integrating B models and environment assumptions and constraints in a single modelling framework (HLL). Our work defined a formal technique, related to model translation, to verify and to validate the safety critical software developed using the B modelling language. HLL language is used as a basis for safety properties verification in order to bridge the gap between the software specification, such as the formal development in B, and the verification techniques on system level. In our work, we proposed a formal framework to guarantee the correctness of the translation from B models to HLL models. The correctness of the translation rules is proven in Isabelle/HOL theorem prover. A proof of equivalence between B and HLL semantics based on a bi-simulation relationship has been set up. It guarantees that the translation rules implemented in the B2HLL tool are correct i.e. semantic preserving according to the defined equivalence relation. The formalization and the associated proofs presented in this work can be easily extended to other transformation from state based language to HLL. The developed approach is currently being integrated in the PERF tool suite used at the RATP company.

As future work, our objective is to extend this verification process to higher abstraction levels of B developments (refinements). Such an extension offers the capability to perform formal verification at early stages of the development and avoid time and resource consuming verification at code level. Our approach consists in seeing operations (functions and procedures) as black boxes abstracted by their before-after predicates. The main difficulty remains in formalizing abstract and concrete variables together with the gluing invariants.

Fig. 1 .

 1 Fig. 1. A formal framework of certified translator

  IMPLEMENTATION T r a i n P o s i t i o n i n g . . . INVARIANT / * Typ1 * / t _ s e g m e n t = 1 . . c_nb_segments / * Typ2 * / t _ d e p l a c e m e n t = 0 . . c_max_dep / * Typ3 * / t _ a b s c i s s e = 0 . . c_segment_length / * Inv1 * / v_segment ∈ t _ s e g m e n t / * Inv2 * / v _ s e g m e n t _ b e f o r e ∈ t _ s e g m e n t / * Inv3 * / v_absOnSegment ∈ t _ a b s c i s s e / * Inv4 * / v_absOnSegment_before ∈ t _ a b s c i s s e / * UnitReq1 * / ( v _ s e g m e n t _ b e f o r e * c _ s e g m e n t _ l e n g t h ) + v_absOnSegment_before ≤ ( v_segment * c _ s e g m e n t _ l e n g t h ) + v_absOnSegment / * UnitReq2 * / ( v _ i s S e g m e n t F o u n d = TRUE ⇒∃dd . ( dd ∈ t _ d e p l a c e m e n t ∧ ( v_segmentv _ s e g m e n t _ b e f o r e ) * c _ s e g m e n t _ l e n g t h + v_absOnSegment = v_absOnSegment_before + dd ) ) / * UnitReq3 * / ( v_isSegmentFound = FALSE ⇒ ( v _ s e g m e n t _ b e f o r e * c _ s e g m e n t _ l e n g t h ) + v_absOnSegment_before = ( v_segment * c _ s e g m e n t _ l e n g t h ) + v_absOnSegment ) . . . Listing 1. B TRPL Invariants OPERATIONS f i n d L o c ( i _ s e g , i _ a b s , i _ d e p ) = VAR l_x , l _ s e g IN l _ x:= i _ a b s + i_dep ; l _ s e g:= i _ s e g ; WHILE c _ s e g m e n t _ l e n g t h < l _ x ∧ ( l _ s e g < c_nb_segments ) DO l _ x:= l _ xc _ s e g m e n t _ l e n g t h ; l _ s e g:= l _ s e g + 1 INVARIANT l _ s e g ∈ t _ s e g m e n t ∧ l _ x ∈ NAT ∧ i _ s e g ∈ t _ s e g m e n t ∧ i _ a b s ∈ t _ a b s c i s s e ∧ i _ d e p ∈ t _ d e p l a c e m e n t ∧ ( l _ s e gi _ s e g ) * c _ s e g m e n t _ l e n g t h + l_x = i _ a b s + i_dep VARIANT l _ x END ; v_isSegmentFound:= bool ( c _ s e g m e n t _ l e n g t h ≥ l _ x ∧ ( l _ s e g ≤ c_nb_segments ) ) ; IF ( v _ i s S e g m e n t F o u n d = TRUE) THEN v_absOnSegment:= l _ x ; v_segment := l _ s e g END END . . . END Listing 2. B TRPL Operations

  t_segment ; i n t [ 0 , c_max_dep ] t _ d e p l a c e m e n t ; i n t [ 0 , c_segment_length ] t _ a b s c i s s e ; D e c l a r a t i o n s : t _ d e p l a c e m e n t x_deplacement ; D e c l a r a t i o n s : t _ a b s c i s s e v_absOnSeg ; t_segment v_seg ; D e f i n i t i o n s : v_seg_0 := 1 , v_seg ; v_absOnSeg_0 : = 0 , v_absOnSeg ; v_seg := v_segment ; v_absOnSeg := v_absOnSegment ; . . . Proof O b l i g a t i o n s : (1 ≤ v_segment & v_segment ≤ c_nb_segments ) ; / / Inv1 (0 ≤ v_absOnSegment & / / Inv3 v_absOnSegment ≤ c _ s e g m e n t _ l e n g t h ) ; / / UnitReq1 ( p r e ( v_segment , v_seg_0 ) * c _ s e g m e n t _ l e n g t h + p r e ( v_absOnSegment , v_absOnSeg_0 ) ≤ v_segment * c _ s e g m e n t _ l e n g t h + v_absOnSegment ) / / UnitReq2 v_isSegmentFound_1 -> ( ( ( v_segmentp r e ( v_segment , v_seg_0 ) ) * c _ s e g m e n t _ l e n g t h + v_absOnSegment ) = p r e ( v_absOnSegment , v_absOnSeg_0 ) + : : doLoc_0 : : l_xDep_0 ) / / UnitReq3 ~( v_isSegmentFound_1 ) -> ( p r e ( v_segment , v_seg_0 ) * c _ s e g m e n t _ l e n g t h + p r e ( v_absOnSegment , v_absOnSeg_0 ) = v_segment * c _ s e g m e n t _ l e n g t h + v_absOnSegment ) ; / / SystReq v_seg = p r e ( v_seg , 1 ) ∨ v_seg = p r e ( v_seg , 1 ) + 1 ;

  are transformed into HLL Proof Obligations clause encoding the safety properties. All the unitary requirements are derived from the B INVARIANT clause.

  | And bexp bexp | Or bexp bexp | Leq aexp aexp | Eq aexp aexp | Equiv bexp bexp | Lt aexp aexp | Gt aexp aexp | Greq aexp aexp Listing 8. Boolean expressions datatype i n s t r u c t i o n = Bl " i n s t r u c t i o n l i s t " | SKIP | Assign vname exp | I f bexp i n s t r u c t i o n i n s t r u c t i o n Listing 9. Statements 2) B Semantics: The semantics of B constructs is defined using primitive recursive functions encoded in Isabelle/HOL. B expressions are interpreted by the total function meaning_exp ∈ exp → env → val. An expression is evaluated in the environment env. The semantics of B statements is given by the total function meaning_instruction ∈ instruction → env → env. It updates the environment env with the effect of the interpreted instruction. Listing 10 provides the definition of the semantic function meaning_instruction.fun m e a n i n g _ i n s t r u c t i o n : : " i n s t r u c t i o n ⇒ env ⇒ env " where " m e a n i n g _ i n s t r u c t i o n ( SKIP ) σ = σ " | " m e a n i n g _ i n s t r u c t i o n ( Bl l i s t ) σ = ( c a s e l i s t of [ ] ⇒ σ | e#l ⇒ m e a n i n g _ i n s t r u c t i o n ( Bl l ) ( m e a n i n g _ i n s t r u c t i o n e σ ) ) " | " m e a n i n g _ i n s t r u c t i o n ( Assign ( vn , Tval . Bool ) ( Bexp exp ) ) σ = σ ( ( vn , Tval . Bool ) : = B ( meaning_b exp σ ) ) " | " m e a n i n g _ i n s t r u c t i o n ( Assign ( vn , Tval . I n t ) ( Aexp exp ) ) σ = σ ( ( vn , Tval . I n t ) := I ( meaning_a exp σ ) " | " m e a n i n g _ i n s t r u c t i o n ( I f c b1 b2 ) σ = ( i f meaning_b c σ t h e n m e a n i n g _ i n s t r u c t i o n b1 σ e l s e m e a n i n g _ i n s t r u c t i o n b2 σ ) " Listing 10. Semantics of B statements

  o o l s t r e a m " | Neq aexp aexp | Bvar vname | Not bexp | And bexp bexp | Or bexp bexp | Leq aexp aexp | Eq aexp aexp | Equiv bexp bexp | Lt aexp aexp | Gt aexp aexp | Greq aexp aexp bexp exp exp datatype i n s t r u c t i o n = Bl " i n s t r u c t i o n l i s t " | Assign vname exp | Assign ' vname exp exp Listing 15. Expression and Statements

  fun stream_comp : : " v a l ⇒ v a l ⇒ v a l " where " stream_comp (B v1 ) (B v2 ) = B( λ i . i f i =0 th e n v1 0 e l s e v2 ( i -1) ) " | " stream_comp ( I v1 ) ( I v2 ) = I (λ i . i f i =0 th e n v1 0 e l s e v2 ( i -1) ) " Listing 16. Flow composition fun meaning_exp : : " exp ⇒ env ⇒ v a l " where " meaning_exp ( Bexp ex ) σ = B ( meaning_b ex σ ) " | " meaning_exp ( Aexp ex ) σ = I ( meaning_a ex σ ) " | " meaning_exp ( I f c b1 b2 ) σ = ( l e t ( val1 , v a l 2 ) = ( ( meaning_exp b1 σ ) , ( meaning_exp b2 σ ) ) in ( c a s e ( val1 , v a l 2 ) of (( I b1) , (I b2)) ⇒ I (λ i . ( i f meaning_b c σ i t he n b1 i e l s e b2 i ) ) | ((B b1) , (B b2)) ⇒ B (λ i . ( i f meaning_b c σ i t he n b1 i e l s e b2 i ) ) ) ) " Listing 17. Semantics of HLL Expressions

  fun T r a n s f o r m a t i o n : : " b . i n s t r u c t i o n ⇒ mapping ⇒ ( h l l . i n s t r u c t i o n × mapping ) " where " T r a n s f o r m a t i o n ( b . Bl [ ] ) m = ( h l l . Bl [ ] , m) " | " T r a n s f o r m a t i o n ( b . Bl ( a# l i s t ) ) m = ( comp ( T r a n s f o r m a t i o n a m) ( T r a n s f o r m a t i o n ( b . Bl l i s t ) ) ) " | " T r a n s f o r m a t i o n b . SKIP m = ( h l l . Bl [ ] , m) " | " T r a n s f o r m a t i o n ( b . Assign vname exp ) m = ( l e t v = ( c r e a t e F r e s h H L L V a r i a b l e vname m) i n ( h l l . A s s i g n v ( T_exp exp m) , m( vname→ ( v , v ) ) ) ) " | " T r a n s f o r m a t i o n ( b . I f bexp i n s t r u c t i o n 1 i n s t r u c t i o n 2 ) m = ( l e t ( * c ' =⇒ C o n d i t i o n t r a n s f o r m a t i o n * ) c ' = ( T_exp ( b . Bexp ( bexp ) ) m) ; ( * c1 =⇒ IF b l o c k t r a n s f o r m a t i o n and m1 =⇒ R e s u l t i n g mapping * ) ( c1 , m1) = T r a n s f o r m a t i o n i n s t r u c t i o n 1 m; ( * c2 =⇒ E ls e b l o c k t r a n s f o r m a t i o n and m2 =⇒ R e s u l t i n g mapping * )( c2 , m2) = T r a n s f o r m a t i o n i n s t r u c t i o n 2 (m ⊗ m1 ) ; ( * v a r s =⇒ M o d i f i e d v a r s i n one o f IF branches * ) v a r s = {v . v : ( dom m) ∧ ( (m v = m1 v ) ∨ (m v = m2 v ) ) } ; i n s t = λ i v . ( c a s e ( snd v ) o f Tval . Bool ⇒ ( h l l . Bexp o h l l . Bvar ) | Tval. Int ⇒ h l l . Aexp o h l l . AVar ) ; ( * s t =⇒ F in a l s t a t e a f t e r IF * ) s t = F i n i t e _ S e t . f o l d ( T _ i f _ s t e p _ s t ) m2 v a r s ;( * L i s t o f a s s i g n s f o r m d i f i e d v a r s * ) a s s i g n s = F i n i t e _ S e t . f o l d ( T _ i f _ s t e p _ i m1 m2 i n s t c ' s t ) {} v a r s i n ( Bl ( [ c1 , c2 ]@( s e t _ t o _ l i s t a s s i g n s ) ) , s t ) ) " Listing 19. B to HLL Transformation Function in Isabelle/HOL The transformation functions are defined inductively on the syntactic constructs of the B modelling language. Listing 19 shows the definition of transformation functions in Isabelle/HOL.


Reza Russell Hatami
email: russell.hatami@hiof.no

Johanna Pejlare
email: pejlare@chalmers.se

Rizanesander

Rizanesander's Recknekonsten or "The art of arithmetic" -the oldest known textbook of mathematics in Swedish

Keywords: Mathematics history, history of education, arithmetic, mathematics education

de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Swedish school mathematics has a history of about four centuries. During recent years there has been an increased research interest in the history of Swedish mathematics education (see, for example, [START_REF] Hatami | Reguladetri: en retorisk räknemetod speglad i svenska läromedel från 1600talet till början av 1900-talet[END_REF], [START_REF] Lundin | Skolans matematik: en kritisk analys av den svenska skolmatematikens förhistoria, uppkomst och utveckling[END_REF], [START_REF] Pejlare | On the relationships between the geometric and the algebraic ideas in Duhre's textbooks of mathematics, as reflected via Book II of Euclid's Elements[END_REF], and [START_REF] Prytz | Speaking of Geometry: a study of geometry textbooks and literature on geometry instruction for elementary and lower secondary levels in Sweden, 1905-1962[END_REF]). However, not much research has been conducted on the early history of Swedish mathematics education. The first printed textbook on arithmetic in Swedish was written by Aegidius Aurelius (c.1580Aurelius (c. -1648) ) in 1614 [START_REF] Aurelius | Minnen och dokument. 5[END_REF]. However, the oldest known manuscript in Swedish of a mathematics textbook was written in 1601 by Hans Larsson Rizanesander (1574Rizanesander ( -1646)); this manuscript is the focus of the present paper. The manuscript, entitled Recknekonsten (The art of arithmetic), constitutes a significant part of the history of Swedish mathematics education. There seems to be a pedagogical idea behind the structure of the text, and it contains numerous examples with solutions. Even though it was never printed, and it is not known to what extent it was used, it can give us insights into the early history of Swedish mathematics education. Hatami and Schéele have interpreted the handwritten manuscript, and in 2018 it was, after more than 400 years, finally printed [START_REF] Rizanesander | Recknekonsten -Tolkad av Reza Russell Hatami & Adam von Schéele[END_REF]. Hultman (1868[START_REF] Hultman | Svenska aritmetikens historia[END_REF][START_REF] Hultman | Svenska aritmetikens historia[END_REF] wrote on the Swedish history of arithmetic, but he was probably not aware of Rizanesander's manuscript, since it was not mentioned. In his dissertation on the Swedish history of mathematics up to 1679, [START_REF] Dahlin | Bidrag till de matematiska vetenskapernas historia i Sverige före 1679[END_REF] summarized parts of Rizanesander's manuscript, but he did not consider it in the context of the Swedish history of mathematics education. The present paper is part of the outcome from a larger project aiming to contribute to the understanding of the early history of mathematics education in Sweden. The aim of this paper is to investigate Rizanesander's manuscript as well as possible influence on him by other authors. We conduct a content analysis on relevant parts of the manuscript and perform comparisons to other textbooks on arithmetic that he may have had access to. In order to better understand the context in which Rizanesander wrote his manuscript, we will first give an overview of the Swedish history of mathematics education (13 th to 17 th century).

Swedish history of mathematics education

To better understand the cultural value of Rizanesander's manuscript and its importance for mathematics education, we will first give a summary of the history of Swedish mathematics education until the 17 th century. The Swedish education has its origin in the 13 th century, when education was committed at cathedral schools, convent schools and provincial schools. Through the Fourth Council of the Lateran, convoked by Pope Innocentius III in 1215, each cathedral was committed to have a school where future priests could get free education. In 1237 the Dominican Order established the first Swedish convent school in Åbo. The convent schools were oriented towards theology, but gave a higher education than the cathedral schools. In particular, those belonging to the higher states had the possibility to get educated. However, many nobles on the continent could not read or write and possibly it was the same in Sweden. During the reformation in the 16 th century the convent schools were closed and the opportunity of higher education disappeared. King Gustav Vasa (1496-1560) took over the management of the cathedral schools and provincial schools, but there was no particular interest of education among the people. Not until 1842 there was a Royal decision to implement a public-school system in Sweden [START_REF] Lundgren | When curriculum theory came to Sweden[END_REF].

The oldest university in the Nordic countries is Uppsala University, which was founded in 1477, and it was the only university in Sweden until King Gustav II Adolf in 1632 founded the university of Dorpat, which today is the University of Tartu in Estonia. During the Reformation there was very little activity at Uppsala University, but during the synod of the Lutheran Church of Sweden in 1593 the Duke Charles (later King Charles IX) gave new privileges to the university, which reopened in 1595 [START_REF] Pejlare | On the relations between geometry and algebra in Gestrinius' edition of Euclid's Elements[END_REF]. Until the reformation the traces of mathematical knowledge in Sweden are few; only at the end of the 13 th century the Arabic numerals became known [START_REF] Dahlin | Bidrag till de matematiska vetenskapernas historia i Sverige före 1679[END_REF]. At the beginning of the 14 th century there probably were a few that were skilled in using the Arabic numerals in simple calculations, but at the beginning of the 16 th century there were most likely very few Swedes who could perform calculations except with finger calculations or with an abacus.

The first Swede mentioned to own mathematical literature is the canon Hemming from Uppsala, who testamented his mathematics books to a relative when he died in 1299. Among these books we find those written by two of the most well-known mathematicians of that time: Campanus of Novara (c. 1220-1296) and Johannes de Sacrobosco (John of Halifax, c.1195-1256) [START_REF] Dahlin | Bidrag till de matematiska vetenskapernas historia i Sverige före 1679[END_REF]. The oldest Swedish mathematical work known is a short overview of the calendar with the title Tabula cerei paschalis, written in Uppsala in 1344. The first Swedish mathematician mentioned to have been relatively knowledgeable of mathematics and astronomy is King Charles VIII (c. 1408-1470), but some details of what kind of knowledge he had is not known.

When Uppsala University was given new privileges in 1593, Ericus Jacobi Skinnerus (deceased 1597), became the first Swedish professor of mathematics [START_REF] Rodhe | Matematikens utveckling i Sverige fram till 1731[END_REF]. No mathematical works by Skinnerus have been encountered. Nevertheless, he was an avid supporter of the French philosopher Petrus Ramus' (1515-1572) controversial ideas [START_REF] Rodhe | Matematikens utveckling i Sverige fram till 1731[END_REF]: Ramus questioned the Aristotelian theories that were then dominating in the academic world. Even if we cannot see any clear traces of mathematical activity during the time of Skinnerus, his interest of ramism should have provided a basis for a positive development of education.

The first Swedish professor of mathematics whose activity we know somewhat well is Laurentius Paulinus Gothus (1565-1646). He was a professor at Uppsala University from 1594 to 1601 where he lectured on arithmetic, algebra, logic, geometry and philosophy [START_REF] Dahlin | Bidrag till de matematiska vetenskapernas historia i Sverige före 1679[END_REF]. He also studied the mathematical works by Ramus, and in his spirit Paulinus struggled for the Aristotelian theories to be removed from school. Ramus preached on the usefulness of science, which for mathematics implies the search for applications to other subjects. The followers of Ramism in particular fought the mysterious and superstitious features found in the Aristotelian scholastics [START_REF] Rodhe | Matematikens utveckling i Sverige fram till 1731[END_REF]. In 1637 Paulinus became arch bishop and promulgated a program for students of theology: the demand for becoming a priest would be to have good knowledge of arithmetic, Euclid's Elements, Ramus' physics and in astronomy, in particular the doctrina sphaerica and the calendar [START_REF] Dahlin | Bidrag till de matematiska vetenskapernas historia i Sverige före 1679[END_REF].

During the end of the 16th century it became possible to teach mathematics at the cathedral schools as long as the teaching did not have a negative influence on other subjects. In the curricula from 1611, Skolordningen 1611, we can read that in school the children should be educated in Buscherus' arithmetic and in "Sphaera Johannis de Sacro busto" with the condition that no other subjects would be neglected [START_REF] Dahlin | Bidrag till de matematiska vetenskapernas historia i Sverige före 1679[END_REF]. Buscherus, or Heizo Buscher (1564-1598), was a German philosopher. His book on arithmetic, Arithmeticae logica methodo conscriptae libri duo (1590), was an important textbook in Sweden during the early 17 th century [START_REF] Vanäs | Divisionens historia i Sverige[END_REF] and was later reedited by the Swedish bishop Johannes Bothvidi (1575-1635). Johannis de Sacro busto most likely refers to Johannes de Sacrobosco, who wrote a book on astronomy, Libellus de sphaera, that was widely used at universities during the middle ages.

The first known mathematics book on arithmetic in Sweden is a handwritten manuscript in Latin on the rule of three, by Peder Månsson (c.1465-1534), written in the early 16 th century [START_REF] Hultman | Svenska aritmetikens historia[END_REF]. In 1609 Olof Bures' (1578-1655) book on arithmetic, Arithmetica instrumentalis abacus, was printed. The first printed textbook on arithmetic in Swedish is Aegidius Aurelius' Arithmetica eller Räknebook, medh heele och brutne Taal (Arithmetica or arithmetic textbook, with integers and fractions), which was published in eleven editions between 1614 and 1705. But already in 1601, the first Swedish textbook on arithmetic was written: Recknekonsten by Hans Larsson Rizanesander. It is written in Swedish at a time when education was reserved for privileged boys with knowledge of Latin, and when mathematics education still was not generally in question.

Rizanesander and Recknekonsten

Not much is known about Hans Larsson Rizanesander (1574Rizanesander ( -1646)). He studied at Vasa Akademi in Gävlea school that had been founded by King Gustav Vasa in 1557and became a judge in Gästrikland, a province north of Uppsala, in 1605. Originally, he came from Rotskär in Älvkarleby. The linguistic origin of the name Rizanesander is a Greek translation of the Swedish word Rot-skärman (in English: Root-skerry-man), i.e., Rhiza-nes-ander.

Rizanesander wrote his manuscript in Tallinn, which during this time was a dominion of Sweden called Räffle or Reval. Today the manuscript is kept at the university library Carolina Rediviva at Uppsala University; to our knowledge it only exists in one copy. The manuscript is dated the 21 st of August 1601. It does not have a title, but since the word Recknekonsten (The art of arithmetic) is used in the dedication this is how we will refer to the book. The manuscript consists of 147 pages, including twelve pages that may have been written by Rizanesander's son Lars Hansson. It is divided into 20 chapters: The first two chapters contain definitions and explanations of the hinduarabic positional notation (4 pages), as well as a description of the abacus (4 pages). The following four chapters deal with addition (11 pages), subtraction (7 pages), multiplication (10 pages) and division (12 pages), both on the abacus and with numerals. Chapters VII and VIII deal with the greatest common divisor (1 page) and the least common multiple (4 pages). Chapters IX to XIII deal with fractions (3 pages) and the four basic mathematical operations with fractions (5, 4, 3, and 4 pages, respectively). Chapter XIV deals with arithmetic and geometric series (10 pages), and chapters XV and XVI deal with the rule of three (14 pages) and reversed rule of three (2 pages). The last four chapters deal with general counting (3 pages), square roots and cubic roots (19 pages), regula cecis (also called regula virginum, 7 pages), and the rule of false position (8 pages).

The manuscript is dedicated (4 pages) to Duke John (1589-1618), son of King John III of Sweden. At this time Duke John was 12 years old. In the introduction Rizanesander claims that the art of arithmetic is indeed a glorious and useful art, since God herself used arithmetic. He also refers to Plato, who demanded that kings and princes should have the acquirement of the art of arithmetic. At the end of the introduction Rizanesander asks Duke John for financial support in order to have the manuscript printed. It is not known if there was any contact between Rizanesander and Duke John, but apparently Rizanesander never got any funding, since the manuscript was not printed. It is not known if Duke John ever mastered the art of arithmetic. However, he never became king; twice he gave up the throne and he died only 28 years old.

Recknekonsten or The Art of Arithmetic

Rizanesander begins the first chapter of Recknekonsten by stating that "The art of arithmetic is a knowledge of calculating well"1 . He uses nine significant digits (1-9) and one insignificant (0) called Nulla or Ziphra. 2 The insignificant is explained to "do nothing by itself"3 but it fills up the space where there is no significant digit. This means that the zero only has a meaning as an empty place indicator in the place value number system; the zero does not yet have a meaning in itself. These ten significant and insignificant digits are explained to be "the wood of the art of arithmetic of which it is built in the same way as a house is built by timber, stones, lime, clay and sand"4 . It is further explained how numbers should be pronounced. Rizanesander does not have a word for numbers greater than 1000. To pronounce a great number, he uses a dot on each thousand to indicate how many multiples of thousand the digits represent. The example he gives, , should be pronounced as follows:

Thirteen thousand, thousand thousand, thousand thousand times thousand Four hundred fiftysix thousand thousand thousand, thousand times thousand […] four hundred eighty nine5

This method is not very efficient, but any great number can be pronounced with it. In Christopher Clavius' (1537-1612) Epitome arithmeticae practicae from 1583 great numbers were also marked with dots and described to be pronounced in the same way.

After presenting numbers and how to pronounce them, Rizanesander continues to give a description of the abacus (see Figure 1) and the meaning of the lines and their spacing on it. A coin on the lines represents, from below, a unit, a tenth, a hundredth and so on. A coin in the spaces between the lines represents five, fifty, five hundred, and so on. His abacus resembles a traditional abacus but with the supplement that a coin below the bottom line represents half a unit. This is interesting, considering that Rizanesander has not yet introduced fractions. Rizanesander proceeds through the following four chapters by explaining the four basic operations addition, subtraction, multiplication and division, both with the abacus, and with algorithms. The abacus will only be used in these chapters; in later chapters numerical methods, only, will be considered. The chapters on the four basic operations with numbers include many examples. Most of the examples concern money, but there are also some numerical examples without a context where it is explained how to carry through the algorithms.

The algorithm for the addition of numbers is the same as the standard addition algorithm that we use today, starting from the right. However, when Rizanesander describes subtraction with numbers, he starts the algorithm from the left, which forces him at each step to look at the position to the right in order to decide whether he has to decompose and recompose the numbers or not. For example:

One asks how many years there has been since we wrote 1574 and now write 1601? Reliquus 27.

Put

. Say 1 from 1 is nothing left. Draw a line through them both. Say again 5 from 6

Reliquus is 1, which should be written above. But the next number, 7 could not be taken from 0. Therefore, write under :| less than one is 0 |: and keep this. Draw a line through 6 and 5. Say again from 10 :| Since you had it in memory to do so |: Reliquus is 3. But write less that is 2 above, the same reason as before, draw a line through 0 and 7, and again keep one in memory; Thereafter take four from 11 Reliquus is 7 which can complete be written above. Draw a line through 1 and 4 and now the example is thus: .6

Ramus used the same algorithm for subtraction in his Arithmeticae libri from 1555, but Clavius in 1583 used the same subtraction algorithm as we do today.

Chapter V deals with multiplication, and this chapter Rizanesander begins by presenting the Pythagorean table (see Figure 2), which he states has to be learned by heart. Interesting is that Rizanesander uses a triangular table, where the commutative law implicitly has to be considered. This means that from the table of multiplication with 2 to the table of multiplication with 9 the length of the tables successively gets shorter. Also, other mathematicians active during the 17 th and first half of the 18 th century, such as for example Aurelius, but also Nils Buddaeus Rizanesander refers to the Pythagorean table when he describes division with numbers. The division algorithm with numbers he uses is a scratch method, or divisione per galea, which was a common method in the middle ages [START_REF] Vanäs | Divisionens historia i Sverige[END_REF]. Characteristic for this method is that the divisor is written under the dividend and is moved one position for every new quotient digit, and the quotient is written to the right. As the computation is performed, the digits belonging to the same number does not have to be written next to each other on the same line and the remainder is written above the dividend. Also, the partial products are computed from the left to the right and are subtracted as they are computed.

After the chapters on the four basic mathematical operations, Rizanesander proceeds with finding the greatest common divisor, and the least common multiple, of two numbers. He needs this in his rendering of fractions and the four basic mathematical operations with fractions in the following chapters. Compared to the presentation of the four basic operations with numbers, the presentation of the four basic operations with fractions is different. Both presentations contain numerous Dragh och een Linie igenom 1 och 4 och ståår nu hele Exemplett såledhes. (Rizanesander, 1601, p. 14 v-15 r).

examples, but when the examples with numbers often are in a context there is, with only one exception (unit weights), no context in the examples with fractions. Also, there is no explanation of how the fractions should be interpreted: focus lies instead on how the algorithm should be carried through. However, in the following chapter XIV on arithmetic and geometric series we find examples where fractions are used in a context. One example of an arithmetic series is the following:

I would like to know how many times the bell rang since it rang at one during the night until it rang at 12 during the day. 7 Many of the examples use a context with money. The money used in Sweden at this time was thaler, mark, öre and penningar (pg). The thaler was an international silver coin used throughout Europe. One thaler is four mark, one mark is eight öre, and one öre is 24 penningar. One example of a geometric series in the context of money, which resembles an example we also find in Buscherus' Arithmeticae (1590), is the following:

One buys a horse that is shoed with 32 nails and give 1 pg for the first nail, 2 pg for the second nail, 4 pg for the third nail and 8 for the fourth and so on doubling. How expensive is the horse? Answer: pg, that is thaler 1 mark 6 öre 19 pg. That was an expensive horse. 8 This was indeed an expensive horse. But Rizanesander has actually made an arithmetical mistake when he changes his money: the correct answer should be 5,592,405 thaler, 1 mark, 2 öre and 15 penningar.

Concluding remarks

Being the oldest mathematics textbook in Swedish, Rizanesander's manuscript is an important source through which we can learn more on the early Swedish history of mathematics education. The manuscript includes a rich repertoire of examples, giving students the possibility to master the art of arithmetic. However, explanations to, for example, why certain algorithms work, are not given. Regarding the algorithms, we see some similarities with both Ramus' and Clavius' books, indicating that Rizanesander was influenced by them. Also, it is indicated that he was influenced by Buscherus' book. We suggest that further investigations of Rizanesander's manuscript should be done; in particular it would be valuable to consider not only the algorithms, but also the contextualization of the examples in order to further investigate in what way he was influenced by Ramus, Clavius and Buscherus.

Figure 1 :

 1 Figure 1: Rizanesander's abacus representing the number 268,957,129 (Rizanesander, 1601, p. 6 r).

Figure 2 :

 2 Figure 2: Rizanesander's table of multiplication (Rizanesander, 1601, p. 16 r).

  , Nicolaus Petri Agrelius (c. and Anders Celsius (1701-1744), have taken the commutative law into account when they designed their multiplication tables, which makes the table triangular and compact. However, Swedish mathematics textbook authors during the end of the 18 th century, such as Nils Petter Beckmarck (1753-1815), Olof Hansson Forsell (1762-1853) and Per Anton Zweigbergk (1811-1862) used quadratic multiplication tables and do not focus on the commutative law. Clavius (1583) also used a quadratic multiplication table, but Ramus (1555) only presented a multiplication algorithm and not a multiplication table.

  skriffwas offwanföre. Men her till nest föliande taal, icke kunna 7 tages vthaf 0. Derföre skriff ret vnnder :| mindre ähn eett ähr 0 |: och beholtt thz. Dragh een linie igenom 6 och 5. Sägh åther ifrå 10 :| Ty war thu i sinnett hadhe gör thz så |: Reliquus ähr 3. Men skriff i mindre som ähr 2 offwanföre, för förne orsackz skuldh; drag een linie igenom 0. Och 7, och beholtt åther eet i sinnett; Tagh sidhan fyra ifrå 11 Reliquus ähr 7 hwilken kan fulkommeligen schriffwas offwan före.

"Recknekonsten ähr een lärdom till att wäll Reckna"(Rizanesander, 1601, p. 3 r).

In modern Swedish the word for zero is noll and the word for numerical digit is siffra.

"förmå inthett vthi sig sielff" (ibid, p. 3 r).

"wirkin till Reckne konsten af hwilken hon warder vpbÿgd medh Lijka såsom till itt hus att vpbyggia hörer Stocker, Stenar, Kalck, Leer och Sandh" (ibid, p. 3 r).

Thretton tusendh, tusend tusend, tusend tusend gånger tusend fyre hundrade femtiyosex tusend tusend tusend, tusend gånger tusend […] fyre hundrade ottotiye niyo (ibid, p. 4 v).

Een frågar huru månge åhr, ähre sedan thz skreffz 1574 och nu skriffwes 1601? Reliquus 27. Sätt såledhes. . Sägh 1 ifrå 1 ähr inthz öffwer. Dragh så en linie igenom them bådhen. Sägh åther 5 ifrå 6 Reliquus ähr 1, hwilkett skulle

Acknowledgement

This work was partly supported by the Swedish Research Council [Grant no. 2015-02043].


Bert Zwaneveld

Dirk De Bock
email: dirk.debock@kuleuven.be

Lucas Bunt and the rise of statistics education in the Netherlands

Keywords: Mathematics curriculum, Probability, Secondary school mathematics, Statistics

We describe the role of Lucas Bunt at the start of the teaching of probability and statistics in the last two years of Dutch secondary schools in the early 1950s. Together with his co-authors, Bunt developed an experimental text which, from the mid-1950s on, became a regular textbook. We further sketch Bunt's othermostly internationalactivities with respect to the curriculum reform movement initiated at the Royaumont Seminar in 1959. Bunt's experiment can be seen as one of the initiatives related to this reform. Finally, we present what happened with statistics teaching in the Netherlands "after Bunt".

Introduction

The attention to statistics in Dutch secondary school mathematics arose in the early 1950s when a student text about statistics was developed by a group of mathematics teachers led by Lucas Bunt. The text was used in experiments in the last two years of secondary schools that prepare students for the university, initially only for the non-exact streams of these schools. Bunt's reason to develop this text was a proposal made by Liwenagel, one of the two associations of teachers of mathematics at that time1 , to include statistics into the curriculum for these students. The proposal cannot be seen independently from the worldwide trend after World War II to include applications of mathematics into the secondary school curricula (De Bock & Zwaneveld, in press). During the 1950s the call for curriculum change was so strong that the OECD took the initiative to organize, in 1959, the Royaumont Seminar with representatives from different western countries to initiate the reform. Bunt attended "Royaumont" and many other international meetings related to this reform movement. Although Bunt's pioneering role in statistics education is well-known in the Netherlands, a proper scientific review of his work is still missing. Moreover, his acting at the international math educational scene was not given appropriate attention so far, especially in the debates about a possible introduction of statistics at the secondary school level.

We present Bunt's role in the Dutch curriculum reform movement of the 1950s, more specifically, his activities related to the development of a statistics program as a part of it. Based on written historical sources and a few oral testimonies of contemporaries, we first provide some elements of Bunt's professional career. We then report about his experiment with the teaching of statistics in secondary school classrooms and about the actions he took to ensure that his ideas became consolidated. Finally, we report what happened with statistics in Dutch secondary mathematics curricula "after Bunt" and we present some conclusions.

Lucas Bunt

Lucas Nicolaas Hendrik Bunt (Figure 1) was born in 1905 in Edam, a small village north of Amsterdam. He studied mathematics at the University of Amsterdam where he also defended, in 1934, his PhD thesis, entitled Bijdrage tot de theorie der convexe puntverzamelingen [Contribution to the theory of convex point sets]. In the early 1930s, Bunt started his career as a mathematics teacher in Leeuwarden where he likely met his wife, a chemistry teacher at the same school. In the late 1940s Bunt became mathematics teacher trainer at the University of Groningen. From 1948 to 1969 he was appointed as a full-time mathematics teacher trainer at Utrecht University, a position that he combined with that in Groningen. In 1968, immediately after the retirement of his wife, he and his family migrated to Arizona (US) where Bunt became a professor of mathematics at Arizona State University. We assume that Bunt had already developed strong professional ties with the US in the early 1960s to secure this appointment, but could not verify this any further. Bunt died in 1984 in the US. Bunt became active at the math educational scene in the Netherlands shortly after World War II as a member of the Mathematics Working Group, a group that critically reflected on the existing secondary school curricula and developed proposals for new curricula (La Bastide-van Gemert, 2015). Bunt's international career started in 1959. Recommended by Hans Freudenthal to the Dutch Ministry of Education, Bunt was one of the three representatives for the Netherlands at the famous Royaumont Seminar and he co-edited the Seminar's Proceedings with Howard F. Fehr (OEEC, 1961). In the late 1960s, Bunt translated and adapted, in cooperation with Harrie Broekman, a series of booklets that were developed by the School Mathematics Study Group in the US. This resulted in a six-volume programmed instruction course for Dutch secondary school students.

Bunt was primarily a mathematician who explained mathematics to a non-mathematically schooled audience. We mention his textbook Statistiek voor het voorbereidend hoger en middelbaar onderwijs [Statistics for preparatory higher and secondary education] (1956), intended for Dutch students, aged 16 to 18 years, who prepared themselves for university studies in social sciences, economics, geography, etc., based on an experiment of which Bunt published the report [START_REF] Bunt | Statistiek als onderwerp voor het gymnasium A: verslag van een proefneming[END_REF]. For an international audience, Bunt (co-)authored An introduction to sets, probability and hypothesis testing (with Howard F. Fehr and George Grossman) (1964) and Probability and hypothesis testing (1968).

First experiments with statistic education at the secondary level

Bunt took the initiative to develop an experimental text about statistics in some gymnasia A2 . The text was initially mimeographed, in 1956 it was printed as a textbook [START_REF] Bunt | Statistiek voor het VHMO[END_REF]. As mentioned before, one of the reasons for Bunt to start with an experiment about the teaching of statistics was a proposal of a commission established by the organization of mathematics teachers Liwenagel, intended to study the opportunities and possibilities of "a re-organization of mathematics education in the A-streams of the gymnasia and the gymnasium sections of the lyceums" (1950). Bunt was a member of that commission and, although it is not mentioned, likely the main author of the commission's report.

It is worth mentioning that Bunt did not develop the experimental text and the textbook on his own, although this was a common practice in the Netherlands at that time, but in cooperation with a team of teachers. In the Preface of the textbook Bunt wrote (translated from Dutch):

… was an educational experiment in statistics, organized by the Department of Didactics of the Pedagogical Institute of the State University of Utrecht. The following teachers cooperated: Dr. Cath. Faber-Gouwentak, Barlaeus-Gymnasium, Amsterdam; Sr. E. A. de Jong, Rectrix [Headmistress] St.-Theresia-Lyceum3 , Tilburg; D. Leujes, Grotius-Gymnasium, Delft; Dr. H. Mooy, Barlaeus-Gymnasium, Amsterdam; Dr. P. G. J. Vredenduin, Co-rector [Vice Headmaster] Stedelijk [Municipal] Gymnasium, Arnhem. (Bunt 1956, p. v) At that time in the Netherlands, statistics was not a part of the official curriculum that only included algebra and geometry, topics that were also part of the final exams, organized centrally by the government. However, based on an exception rule, the Inspection of Education could allow teachers to change parts of the exam program. Such exception was obtained for the statistics experiment.

In 1957, Bunt published the report in which he describes the experiment with the student text that was used during the years 1951-1955 [START_REF] Bunt | Statistiek als onderwerp voor het gymnasium A: verslag van een proefneming[END_REF]. The reason why the textbook was published before this report was, as Bunt wrote in the textbook's Preface: "The recent proposals of the mathematics teachers associations Wimecos and Liwenagel about the curriculum change for mathematics in the B-stream of the secondary schools, in which statistics is included as a new topic, made it desirable to make, as soon as possible, the text public" (Bunt, 1956, p. v). Bunt's report has two parts: part A includes the motivation and explanation about the selected topics, and the way they are treated; part B is the student text (it is not included in the printed version of the report).

We focus on some highlights of part A. Bunt motivated the reasons for choosing statistics as follows: to students in university disciplines such as economy, psychology and sociology, an extensive study of algebra is less useful than a well-balanced treatment of the first concepts and principles of statistics. Statistics in university turns out to be very difficult and uncommon to these students. Moreover, they have to learn it in a rather short period of time. Statistics in secondary school is not only useful for the aforementioned students, but for all citizens in modern society. By reducing the algebra content, Bunt found the necessary 35 classroom hours for his statistics course. After that, he justified the chosen topics. In the first experimental text, these topics were: frequency distribution, histogram, frequency curve, cumulative frequency, average, median, quartiles, range, mean deviation, standard deviation, quartile distance, permutations, variations (without repetitions), combinations, Pascal's triangle, Newton's binomial formula, some simple theorems from probability calculus, the binomial distribution for p = 0.5, the normal curve as a limit of the histogram of the binomial distribution (graphical, not with formulae). At the end of the course, some applications of the normal curve for calculating probabilities were presented. Linear regression and correlation were left out, because of being too time-consuming. Especially on the insistence of his cooperators, Bunt drastically changed the end by including a final chapter on hypothesis testing: estimating some characteristics of a population on the basis of a sample.

Bunt extensively deals with the principles of probability calculus for which he presents an axiomatic approach. Probability is a function that assigns to an event a number in the interval [0,1]. He starts from the following two axioms: (1) If p →¬q, then P(p or q) = P(p) + P(q); (2) If p is the sure event, then P(p) = 1. From these axioms Bunt derives the complement and product rule. He illustrates these rules with examples about rolling dice. In the textbook, however, Bunt introduces the concept of probability differently. There he starts with the definition of Laplace: the probability of an event is the number of outcomes favorable for that event, divided by the total number of outcomes (under the condition of mutually exclusive and equally likely outcomes). After having dealt with the complement, the sum and the product rule, he introduces "another" definition: if it turns out that in a large number of repetitions of an experiment, n, an event happens k times, then we are convinced that every time we repeat this experiment a sufficient number of times, this event will happen in k/n part of this number. We then state that the probability of that event equals k/n. For probabilities derived from that "new" definition, the complement, sum and product rule keep their validity. We note that Bunt's approach contrasts sharply with that of his contemporary Gustave Choquet, then president of the International Commission for the Study and Improvement of Mathematics Teaching (CIEAEM), who proposed at the 9 th meeting of the CIEAEM a definition of probability based on the mathematical concept of measure (translated from French):

In a set U, one chooses a family F of subsets E, to each of which we attach a number m(E), called the measure of E. These subsets have the following properties: their union and their intersection are again part of F, even if the number of E's is infinite. In the case of probabilities, the set U has measure m(U) = 1. Each element of U represents a possible event: all favourable events constitute a subset E with measure m(E). The probability of the favourable event is given by m(E)/m(U). (Carleer, 1955-6, pp. 63-64) The difference between Bunt's and Choquet's approaches illustrates the debate during the mid-1950s between the mathematics-didacticians and the mathematics-structuralists on how statistics should be introduced at the secondary school level.

Because of its innovative character, we discuss in some detail how Bunt explained the concept and procedure of hypothesis testing. He wrote about this:

On the basis of a sample of 10 marbles out of a box with 5000 white and 5000 red marbles the probabilities of 0, 1, 2, …, 8, 9, 10 red marbles in that sample are 0.001, 0.010, 0.044, 0.117, 0.205, 0.246, 0.205, 0.117, 0.044, 0.010, 0.001. It follows that in 1.1% of all samples of 10 marbles there are 0 or 1 red marbles, and even so, in 5.5%, there are 0, 1 or 2 red marbles. And, in 5.5% of all samples there are 8, 9 or 10 red marbles. And moreover, in 1.1% of all samples there are 9 or 10 red marbles. Now suppose that the fraction p of red marbles is unknown and we take a sample of 10 marbles. We shall agree that if p = 0.5 and there are 0, 1, 9 or 10 red marbles in the sample, we shall reject the hypothesis p = 0.5. If the hypothesis p = 0.5 is right we have a risk of 1.1% + 1.1% = 2.2% that we, in spite of this, reject the hypothesis. More precisely, there is a probability of 1.1% that we reject the hypothesis p = 0.5 on the strength of too small (or too large) a number of red marbles. Because, in this connection, we, for the time being, do not want to risk a greater probability than 2.5%, we stick to the mentioned agreement. This agreement, therefore, conforms to the following conditions: (a) if p = 0.5, we risk, both for too small and for too large a number of red marbles in the sample, a probability of not more than 2.5% that we reject the hypothesis p = 0.5; (b) both for too small and for too large a number of red marbles this probability lies as close to 2.5% as possible. When we reject the hypothesis p = 0.5, we say the hypothesis p = 0.5 is rejected with an unreliability of not more than 5%. (Bunt, 1957, p. 12) The fraction v is introduced as the number of red marbles divided by the number of marbles in the sample and its values which are or are not thought contradictory to p = 0.5 are represented by, respectively, dots and circles on an axis (Figure 2). Repeating this procedure for different values of p, one gets the two-dimensional scheme (Figure 3): By making the values of v and p "continuous", one gets a figure on which the different boundary lines refer to different sample sizes (Figure 4). The textbook contains two of these, corresponding to unreliabilities of 5% and 10%, called by Bunt "nomograms". From these nomograms, the student can observe that the probability of rejecting a false hypothesis increases with the sample size.

Consolidation and internationalization

In 1954-1955 a curricular commission of Wimecos published a report including a draft curriculum and central examination program for mathematics in HBS-B. Bunt had been a member of that commission representing the Dutch mathematics didacticians and mathematics teacher trainers. In the commission's report, it is stated that statistics had been important sources for the commission. The commission basically confirmed the conclusions of the report of Liwenagel (Liwenagel, 1950(Liwenagel, -1951)), but now generalized to all students who prepared themselves for university studies. In 1958, the new curriculum was actually implemented, but, although it entailed a considerable change, statistics only became an optional subject for gymnasium A.

The fifth edition of Bunt's textbook [START_REF] Bunt | Statistiek voor het VWO[END_REF]) had a slightly different title, a consequence of the curriculum reform consolidated in 1968 by a new law for secondary education. The subtitle, statistics for preparatory higher and secondary education, was changed into: statistics for preparatory scientific education. This new curriculum reform was prepared and supervised by the Commissie Modernisering Leerplan Wiskunde (CMLW) [Commission for Modernization of the Mathematics Curriculum]. The task of that commission was to prepare the mathematics curriculum reform in line with the ideas of Royaumont Seminar. Bunt was a member of the CMLW. The commission was officially set up in June 1961 by the Ministry of Education, Arts and Science, but already in January 1961, Bunt had proposed to the Ministry to establish such commission. However, the Inspection of Education had given a negative advice to the Ministry because the commission as proposed by Bunt was too small. In 1968 the new curriculum for mathematics, in which statistics played a clear role, was implemented in all schools for secondary education in the Netherlands: Bunt had achieved what he had started working on in 1951.

During the late 1950s and early 1960s, Bunt disseminated his ideas about the teaching of statistics. Already on May 24, 1959, he was invited to report on his experiment about the teaching of statistics at the annual meeting of the Société Belge de Professeurs de Mathématiques [Belgian Association of Mathematics Teachers] and the Société Belge de Statistique [Belgian Association of Statistics], held in Brussels on May 24, 1959[START_REF] Bunt | L'enseignement de la statistique dans les écoles secondaires des Pays-Bas[END_REF]. The manner in which statistics became a part of the secondary-school curriculum in the Netherlands was also the topic of Bunt's paper at the Royaumont Seminar (OEEC, 1961). In the period after Royaumont, Bunt had the opportunity to actively participate in meetings held in order to coordinate, monitor and refine the implementation of the Royaumont recommendations (Aarhus, 1960;Athens, 1963, Echternach, 1965).

More recent developments

According to the law for secondary education of 1968, two types of schools could prepare students to higher education: Voorbereidend Wetenschappelijk Onderwijs (VWO, six grades for students from age 12 to 18) [preparatory scientific education], preparing for university studies, and Hoger Algemeen Voortgezet Onderwijs (HAVO, five grades for students from age 12 to 17) [higher general continued education]. The mathematics curricula of these school types were prepared by the CMLW. The curriculum of VWO included probability theory and statistics, that of HAVO only included descriptive statistics. These topics were meant to be taught in the last two years of these school types. We restrict ourselves to statistics teaching at VWO. Although Bunt's textbook was available, CMLW judged that it was better to not implement statistics immediately, but first to develop a new text and conduct an experiment with a restricted number of schools. The argument was that Bunt's textbook was only intended for students in the "old" gymnasia A, whereas statistics now had become a compulsory subject for all students. A statistics development team started in 1970, first under the supervision of the CMLW, from 1971 under the supervision of the then started IOWO, the predecessor of the Freudenthal Institute.

After a first draft the team developed the textbook [START_REF] Nijdam | Statistiek en kansrekening voor het VWO[END_REF] including the following content: Introduction, Probability rules, Probability distributions, Hypothesis testing and reliability intervals, Parameters of a distribution, Use of the normal distribution. The introduction contained an example with a prognosis of the number of students of VWO that should follow science or mathematics at the university, based on data of the Dutch Central Bureau of Statistics. From that example, terms as sample, population, random, representative, testingfor instance with respect to the quality of the production of certain itemswere introduced. In this textbook the students themselves started with a probability experiment. There was a box with 1000 small marbles, 600 red and 400 black. With a kind of spoon with 20 wholes, they drew a random sample of 20 marbles. This box with the "spoon" was used to simulate various probability experiments.

Conclusions

The mathematician Lucas Bunt played a crucial role in promoting and developing materials for statistics education at the secondary level, in the Netherlands but also at the international level. Indeed, in the post-Royaumont era, probability and statistics were seen as valuable elements of a worldwide reform of the mathematics curricula. Although Bunt explained his approach in a rather classical way, starting with some probability axioms (in pure New Math style), the approach in his textbook was very pragmatic. Bunt did not emphasize "theoretical aspects", accepted properties without proof and provided many clarifying examples. This pragmatic style enabled Bunt to explain the basic principles of hypothesis testing at the end of his course, in a limited number of lessons.

Nowadays in the Netherlands and in several other countries, probability and statistics are included in the mathematics programs, at least for some streams at the secondary level, but in the 1950s and 1960s, it was quite revolutionary to propose to teach these topics at that school level.

Because of his didactical work in general and more specifically on statistics, Bunt was important in Dutch mathematical education in the post-WWII period. Due to his participation to Royaumont and other international conferences, and his textbooks in English, Bunt may also have played a role in debates about the gradual introduction of statistical curricula for the secondary school level in other countries. However, this role has not yet been clarified and is a topic for follow-up research.

Figure 1 :

 1 Figure 1: Lucas Bunt (left: detail of a picture of the Mathematics Working Group, 1948; right: attending the public defense of the PhD thesis of his son Harry at the University of Amsterdam, 1981)

Figure 2 :

 2 Figure 2: Axis representing values of v with dots and circles

Figure 3 :

 3 Figure 3: v-axes for different values of p

Figure 4 :

 4 Figure 4: Nomograms for different sample sizes (left, the unreliability is 5%, right 10%)

The other organization of teachers of mathematics was Wimecos. Both organizations, Liwenagel and Wimecos, were the predecessors of the Nederlandse Vereniging van Wiskundeleraren [Dutch Association of Mathematics Teachers].

At that time, the gymnasia in the Netherlands had two study streams: The A-stream, preparing students for university studies such as languages, economics, psychology, sociology, history, and geography, and the B-stream, preparing students for university studies in mathematics, science and technology.

A lyceum was a school for secondary education with two sections: gymnasium and Hogere Burger School (HBS)[Higher Citizens School], similar to gymnasium but without Latin or Greek.

Acknowledgements

We thank Bunt's son Harry for the biographical information about his father, Danny Beckers for the information about the start of the CMLW, and Harrie Broekman for his information about Bunt in the years he was Bunt's colleague at Utrecht University.