 For loops to be reversible, we similarly provide an assertion (the codice_3 after codice_8) and a test (the codice_3 after codice_10).The semantics is that the assertion must hold "only on entry" to the loop, and the test must hold "only on exit" from the loop.In the inverted program, the assertion becomes the test, and the test becomes the assertion.