[doc] Update documentation.

doc/mnist.rst

@@ -4,10 +4,11 @@
 ***********************************
 
 CAISAR provides a convenient way for verifying (local) robustness properties of
-neural networks on datasets, for classification problems only, in a specific
-``CSV`` format. In particular, each of the ``CSV`` lines is interpreted as
+neural networks working on datasets with values in :math:`[0, 1]`, for
+classification problems only. For the moment, CAISAR supports datasets in a
+specific ``CSV`` format only, where each ``CSV`` lines is interpreted as
 providing the classification label in the first column, and the dataset element
-features in the other columns.
+features in the remaining columns.
 
 We recall that a neural network is deemed robust on a dataset element whenever
 it classify with a same label all other elements being at an
@@ -35,7 +36,7 @@ a fragment (:math:`100` images) of the MNIST dataset under the
 ``examples/mnist/csv`` folder. Each line in this file represents an MNIST image:
 in particular, the first column represents the classification label, and the
 remaining :math:`784` columns represent the greyscale value of the respective
-pixels.
+pixels, rescaled into :math:`[0, 1]`.
 
 Properties
 ----------
@@ -121,15 +122,9 @@ dataset, with each element's feature pertubed by :math:`1 \%`, looks like this:
      use caisar.DatasetClassificationProps
 
      goal robustness:
-      let normalized_dataset = min_max_scale true (0.0:t) (1.0:t) dataset in
-      robust model normalized_dataset (0.0100000000000000002081668171172168513294309377670288085937500000:t)
+      robust model dataset (0.0100000000000000002081668171172168513294309377670288085937500000:t)
    end
 
-Note the presence of the ``min_max_scale`` function defined in
-``DatasetClassification`` for normalizing all feature values in :math:`[0,1]`.
-Besides classic *Min-Max scaling*, CAISAR also provides ``z_norm`` function for
-*Z-normalization*.
-
 This file is available, as is, under the ``/examples/mnist/`` folder as
 `property.why
 <https://git.frama-c.com/pub/caisar/-/blob/master/examples/mnist/property.why>`_.