/*
Dit is de mooiste uitwerking die er bestaat
*/

/*
 * inzendcode: 746A04
 * Inzendopgaven hoofdstuk 8 en 9
 * Opgave 2
 */

public class A040{
    public static void main(String[] args) {

	int x = 150,e; // x is een willekeurige invoerwaarde.
//	--pre: x >= 0

/*
############################################################
Bepaal het grootste elf-voud e dat niet groter is dan integer x.
Voor x geldt x >= 0

Strategie:
	Zoek de grootste waarde van e die voldoet aan:
	0 <= e <= x < e + 11
	Een aangezien e een elf-voud moet zijn voegen we hier aan toe:
	^ e MOD 11 = 0

Formele Probleemspecificatie:
	Pre:x >= 0
	Post:0 <= e <= x < e + 11 ^ e MOD 11 = 0

De invariant
	R opschrijven als conjunctie:
	R: e >= 0 ^ e <= x ^ e + 11 > x ^ e MOD 11 = 0

############################################################
1ste operand als variant kiezen:
	I(e): e <= x ^ e + 11 > x ^ e MOD 11 = 0
Stopcriterium:
	e >= 0
	Deze mogelijkheid valt af aangezien de invariant
	impliceert dat e >= 0
############################################################
2de operand als variant kiezen:
	I(e): e >= 0 ^ e + 11 > x ^ e MOD 11 = 0
Stopcriterium:
	e <= x
	B <=> e > x
Toon aan I(e) ^ not B => R
	e >= 0 ^ e + 11 > x ^ e MOD 11 = 0 => e >= 0 ^ e + 11 > x ^ e MOD 11 = 0
	<=>
	true
Initialisitie:
	Omdat e een elf-voud groter dan x moet zijn:
	e = x * 11
	Aangezien x >= 0 geldt nu:
	I(x*11):x*11 >= 0 ^ x*11 + 11 > x ^ x*11 MOD 11 = 0
	Deze bewering levert propositie true op aangezien x >= 0
De stap naar het stopcriterium:
	e telkens verminderen met 11 totdat not B waar wordt:
	--I(e)
	e = e - 11; //stap
	--I(e + 11)
Het herstel van de invariant is niet nodig:
	e >= 0 kan niet verstoord zijn omdat e alleen met 11 wordt verminderd
	 als e > x en aangezien e een elf-voud is kan e (tijdens de loop) niet kleiner
	 zijn dan 11.
	e + 11 > x kan niet verstoord zijn omdat nu de situatie is
	 ontstaan e - 11 + 11 > x <=> e > x <=> B
	En tot slot: e MOD 11 = 0 <=> (e - 11) MOD 11 = 0
	De invariant hoeft dus niet te worden hersteld na de stap.
*/
//	Initialisatie
	e = x * 11;
//	I(x * 11)
	while(e > x)
	{
//	--I(e)
	e = e - 11; //stap
//	--I(e + 11)
//	actie niet nodig
//	I(e)
	}
//	I(e) ^ not B -> R
	System.out.println(e+" is het grootste elf-voud dat niet groter is dan "+x);
/*
############################################################
3de operand als variant kiezen:
	I(e): e >= 0 ^ e <= x ^ e MOD 11 = 0
Stopcriterium:
	e + 11 > x
	B <=> e + 11 <= x
Toon aan I(e) ^ not B => R
	e >= 0 ^ e + 11 > x ^ e MOD 11 = 0 => e >= 0 ^ e + 11 > x ^ e MOD 11 = 0
	<=>
	true
Initialisitie:
	e = 0
	I(0): 0 >= 0 ^ 0 <= x ^ 0 MOD 11 = 0
	Deze bewering levert propositie true op aangezien x >= 0
De stap naar het stopcriterium:
	e telkens vermeerderen met 11 totdat not B waar wordt:
	--I(e)
	e = e + 11; //stap
	--I(e - 11)
Het herstel van de invariant is niet nodig:
	Binnen de loop geldt:
	I(e + 11): e + 11 >= 0 ^ e + 11 <= x ^ e + 11 MOD 11 = 0
*/
//	Initialisatie
	e = 0;
//	I(0)
	while(e + 11 <= x)
	{
//	--I(e)
	e = e + 11; //stap
//	--I(e - 11)
//	actie niet nodig
//	I(e)
	}
//	I(e) ^ not B -> R
	System.out.println(e+" is het grootste elf-voud dat niet groter is dan "+x);
/*
############################################################
4de operand als variant kiezen:
	I(e): e >= 0 ^ e <= x ^ e + 11 > x
Stopcriterium:
	e MOD 11 = 0
	B <=> e MOD 11 > 0
Toon aan I(e) ^ not B => R
	e >= 0 ^ e + 11 > x ^ e MOD 11 = 0 => e >= 0 ^ e + 11 > x ^ e MOD 11 = 0
	<=>
	true
Initialisitie:
	e = x
	I(x): x >= 0 ^ x <= x ^ x + 11 > x
	Deze bewering levert propositie true op aangezien x >= 0
De stap naar het stopcriterium:
	e telkens met 1 verlagen totdat not B waar wordt:
	--I(e)
	e--; // stap
	--I(e-1)
Het herstel van de invariant is niet nodig:
	Binnen de loop geldt:
	I(e-1): e - 1 >= 0 ^ e - 1 <= x ^ e - 1 + 11 > x
*/
//	Initialisatie
	e = x;
//	I(x)
	while(e % 11 > 0)
	{
//	--I(e)
	e-- ; //stap
//	--I(e - 1)
//	actie niet nodig
//	I(e)
	}
//	I(e) ^ not B -> R
	System.out.println(e+" is het grootste elf-voud dat niet groter is dan "+x);

//	--Post:0 <= e <= x < e + 11 ^ e MOD 11 = 0
	}
}