EB2ALL: An Automatic Code Generation Tool - Using Event-B for Critical Device Software Systems - page 114

Ta b l e 7 . 4 Event-B to Java & C# Sets translation syntax

Event-B 'C++' Comment

set_var set <data type> set_var STL library

∪ set_union(...) STL library

∩ set_intersection(...) STL library

\ set_difference(...) STL library

⊆ includes(...) STL library

⊂ includes(...) && !(equal(...)) STL library

⊆ !(includes(...)) STL library

⊂ !(includes(...)) && !(equal(...)) STL library

Event-B 'Java' Comment

set_var Set <data type> set_var =

new HashSet <data type> ()

Java Utilities

∪ unionSet(...) Java Utilities

∩ intersectionSet(...) Java Utilities

\ differenceSet(...) Java Utilities

⊆ isSubset(...) Java Utilities

⊂ isSubset(...) && !(isEqualSet(...)) { Java Utilities

⊆ !(isSubset(...)) Java Utilities

⊂ !(isSubset(...)) && !(isEqualSet(...)) Java Utilities

Event-B 'C#' Comment

set_var HashSet <data type> set_var = .NET Framework 4

new HashSet <data type> ()

∪ UnionWith(...) .NET Framework 4

∩ IntersectWith(...) .NET Framework 4

\ ExceptWith(...) .NET Framework 4

⊆ IsSubsetOf(...) .NET Framework 4

⊂ IsProperSubsetOf(...) .NET Framework 4

⊆ !(IsSubsetOf(...)) .NET Framework 4

⊂ !(IsProperSubsetOf(...)) .NET Framework 4

Before generating a source code from a model, a user is required to refine a sys-
tem using a subset of Event-B symbols (see Tables 7.2 , 7.3 and 7.4 ), which can
restate the model in a more translatable form. Supported symbols are available in
Tables 7.2 , 7.3 and 7.4 . These tables show a set of Event-B syntax to the equivalent
C, C++, Java and C# programming languages. All constants defined in a model's
context must be replaced with their literal values. This translation tool supports Sets
theory notations (not in 'C'), conditional, arithmetical and logical expressions of a