Defining the Java Virtual Machine as Platform for Provably Correct Java Compilation