added some JML for m4