why3/doc/whyml2java.inc

.. _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 <https://www.why3.org/stdlib/mach.java.util.html#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 <https://www.why3.org/stdlib/mach.java.lang.html>`_
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 <https://www.why3.org/stdlib/mach.java.lang.html#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 <https://www.why3.org/stdlib/mach.java.util.html>`_
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() <https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/util/Collection.html#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