.. _sec.java: Compilation of WhyML modules into Java classes '''''''''''''''''''''''''''''''''''''''''''''' The ``java`` extraction driver is used to compile WhyML files into Java classes. The driver does not support `flat` extraction; thus, option ``--modular`` is mandatory. Each (non empty) module `M` is translated into a class with the same name. The imported modules are not translated unless the option ``--recursive`` is used. Since the extraction of a module requires data related to its dependencies, the option ``--recursive`` should be used systematically. The code generated by the Java driver can be tuned using attributes. All attributes used by the Java driver are prefixed with :code:`@java:`. Attributes not encountered in following examples are given in section :ref:`sec.attributes`. In addition to the driver, new modules have been added to the Why3 Standard Library (see :ref:`sec.java-stdlib`). A running example +++++++++++++++++ In order to illustrate the Java extraction, we implement a *directory* of some company. The directory contains *employees* and each of them stores the name of the person and its service in the company, its phone number and the number of its office. We first create the module for the data structure that will store employees; the WhyML code is given below. The module defines a type :code:`t` that is a record with 4 fields, :code:`name`, :code:`room`, :code:`phone` and :code:`service`. For the first three fields, we use types (:code:`integer` and :code:`string`) that mimics those of the Java language; they are defined in modules that come along with the driver (see :ref:`sec.java-stdlib`). The type of the field :code:`service` is defined by an algebraic type. The driver permits to declare inner ``Enum`` classes using algebraic types of the WhyML language. Only algebraic constructors with no arguments are allowed i.e the type is just an enumeration of identifiers. ``Enum`` classes are the only form allowed by the driver. We define a function :code:`create_member` whose purpose is to create a record of type :code:`t`. This function is kinda redundant with the WhyML syntax that permits to build such record directly using the usual constructor (:code:`{ ... }`). The reader should have noticed the attribute :why3:attribute:`java:constructor` attached to the function. It is used to mark functions that should yield Java constructors. The driver allows only such marked functions to build records. .. literalinclude:: javaexamples/directory.mlw :lines: 1-18 :language: whyml We assume that the entire WhyML code described in this section is stored in a file :file:`./directory.mlw`. We generate the file :file:`Employee.java` using the following command (according to the option `-o` the file is created in the current directory). .. code-block:: shell-session $ why3 extract -L . -D java -o . --recursive --modular directory.Employee :why3:tool:`extract` produces the Java code described below. After the header of the class :code:`Employee` comes the definition of the :code:`ServiceId` that correspond to the algebraic type :code:`service_id`. Note that identifiers are translated using camel case. .. literalinclude:: generated/Employee.java :lines: 1-9 :language: java To be consistent with WhyML semantics the fields of the type :code:`Employee.t` have been translated as :code:`final` instance variables. When a field of a record is :code:`mutable` then so is the corresponding instance variable. .. literalinclude:: generated/Employee.java :lines: 11-14 :language: java As a rule of thumb, the first type definition encountered by the driver is assumed to be the type of the generated class. Usually this type is a record, the fields of which are translated as instance variables. Abstract types can also be used when the expected class does not store any data (e.g. an exception) or when one wants to generate an interface (see attribute :why3:attribute:`java:class_kind:`). Since the driver looks for the first type definition, it can be difficult to use module cloning because new types may be added by this mechanism. The definition of a type for the class is not mandatory when one wants to gather a collection of static methods. In order to make generated classes usable with Java containers (especially those implemented in :ref:`sec.java-stdlib`) the driver produces systematically the methods :code:`equals` and :code:`hashCode`. The implementation of these methods for :code:`Employee` objects is given below. These methods are specified :code:`final` to prevent their redefinition. Note that these methods are not available from the WhyML code. .. literalinclude:: generated/Employee.java :lines: 15-51 :language: java Finally the driver translates :code:`create_employee` into a constructor of :code:`Employee` objects. During this translation, the identifier of functions annotated with the attribute :why3:attribute:`java:constructor` is lost. This allows to declare several constructors with different signatures. .. literalinclude:: generated/Employee.java :lines: 53-59,62 :language: java We now focus on the module implementing the directory. We use a :code:`Map` container to associate to a `name` (a :code:`string`) an `Employee`. The container, specified in the module `mach.java.util.Map `_, partially mimics the container from the JDK. A directory is simply a record with only one field :code:`employees` (see section :why3:attribute:`extraction:preserve_single_field` for a detailed description of this attribute). We use the attribute :why3:attribute:`java:visibility:private` to avoid direct access to :code:`employees`. We also define a method :code:`add_employee` that permits to insert a new entry into the directory. The contract of the method requires that no entry already exists the same employee's name and ensures a new entry with given data has been added. .. literalinclude:: javaexamples/directory.mlw :lines: 20-43 :language: whyml The Java code extracted from this specification is the following (the code of methods :code:`equals` and :code:`hashCode` has been suppressed). .. literalinclude:: generated/Directory.java :lines: 1-6,33-42,45 :language: java The reader should have noticed that the contract of :code:`add_employee`. This not surprising since :why3:tool:`extract` removes all `ghost` code. In the context of a WhyML program we are guaranteed that :code:`add_employee` is called with parameters that satisfy the precondition of the function (i.e. :code:`name` is not an entry of the directory). However, if this method is invoked from a client code that has not been generated with :why3:tool:`extract`, we should add explicitly the verification of the precondition. Let fix this issue by modifying :code:`add_employee` in such a way it raises an exception if the precondition is not fulfilled. First, we create the class for the exception :code:`EmployeeAlreadyExistsException`: .. literalinclude:: javaexamples/directory.mlw :lines: 45-57 :language: whyml The creation of an exception for Java extraction is based on two points: #. Firstly, it requires to annotate the module with the attribute :why3:attribute:`java:exception:` *exn-class*. The suffix of this attribute indicates the class from which the generated exception inherits. This suffix is not interpreted and is printed out `as-is` by the driver. In our example, we just want the exception to inherit from the standard :code:`RuntimeException` from the JDK. #. Secondly, the module must define a WhyML exception, :code:`E` in our example. As for standard classes, it is possible to declare instance variables in exceptions. In our example, :code:`EmployeeAlreadyExistsException` stores an information message. .. literalinclude:: generated/EmployeeAlreadyExistsException.java :lines: 1-4,31-40,43 :language: java The implementation of the method :code:`add_employee` can now be updated. First, the contract is changed: the precondition has been removed and replaced by an exceptional postcondition that relates the occurrence of an exception :code:`EmployeeAlreadyExistsException` with an invalid value of the parameter :code:`name`. Then, before the creation of an new entry, we check if :code:`name` already exists in the directory, in which case an exception is raised. .. literalinclude:: javaexamples/directory.mlw :lines: 66-67,76-86 :language: whyml The Java code extracted from this new implementation is given below. Two things have been added to the original method. First, the declaration of the exception in the signature of the function and second, the translation of the test related to the parameter :code:`name`. .. literalinclude:: generated/CheckedDirectory.java :lines: 38-45 :language: java .. _sec.java-stdlib: Extension of Why3 Standard Library ++++++++++++++++++++++++++++++++++ Several modules have been implemented to ease the extraction of Java classes. They are gathered accroding to JDKL's packages. Library `mach.java.lang `_ defines types for bounded integers used in Java (:code:`Short`, :code:`Integer` and :code:`Long`) and also strings (:code:`String`) but the latter are limited to formatting methods. Another important module is `mach.java.lang.Array `_ that must be used in place of Java bounded size arrays. There are also some standard exceptions that are used by others modules. Library `mach.java.util `_ gathers some containers (like :code:`Map` used in this section). In the specification of these containers we tried to stick to Java semantics. In particular, according to the specification of `java.util.Collection.size() `_:: int size() Returns the number of elements in this collection. If this collection contains more than Integer.MAX_VALUE elements, returns Integer.MAX_VALUE. Returns: the number of elements in this collection