Create TODO list from Matthias Güdemann and Yannick Moy remarks on model

Signed-off-by: David MENTRE <d.mentre@fr.merce.mee.com>
Add more detailed explanations of the VC generated for the example

* Answer to a remark made by Matthias GÜDEMANN.

* Give pointer to GNATprove version used to test code.

* Add line numbers to listings.
[GNATprove model] transform Assert into Loop_Invariant to prove one more VC
Add failing test of testing disjunction with a contract case
[GNATprove model] Update TODO
[GNATprove model] Test a pure function with contract for m_per_s_From_km_per_h
[GNATprove model] Use Contract_Cases to express disjonction on transition function
[GNATprove model] update report regarding "transition" function description
[GNATprove model] transform Assert into Loop_Invariant to prove more things
[GNATprove model] Update PDF version of the report