Transcript Java for dummies”

”Java and JMLfor Dummies”
•
The Java source code is
written in a text file using
your favourite editor
(Notepad) and is saved
with extension .java.
Be careful not to save
with extension .java.txt,
but as .java.
I use the JML directory
(next slide).
•
The JML-specification is
written as special
comments in the source
code using ‘/*@...@*/
”Java and JML for Dummies”
•
•
I save source in a
directory in the JMLdirectory.
Be careful not to save
with extension .java.txt,
but as .java.
•
•
My bat-file starts this GUI.
In order to compile my JML-specs, I choose
JML Runtime Assertion Checker Compiler
•
And the RacGUI on next slide opens.
”Java and JML for Dummies”
•
Choose Open File
•
•
A file browser opens, the
wanted source- (.java) files
in your project are selected
and added.
In order to compile (to
generate a .class file) and
to get my JML-specs
checked, I click the ”run”button.
Note the settings:
•
Output on the next slide.
•
”Java and JML for Dummies”
•
During compilation a long
series of messages are
issued. If everything goes
well , it ends with ”Done”.
•
Are there errors in the
spec, error messages are
issued.
”Java and JML for Dummies”
•
Errors in the Java code
also result in error
messages.
”Java and JML for Dummies”
•
Everything went well.
•
An executable (.class) file has
been generated.
•
It is executed using the
command ”jmlrac <class-fil>”
from a prompt. The command
must be issued from the directory
were source and class files are
placed.
Note: the extension (.class) is
omitted.
•
From here the process is
described on the slides
‘JML-1.ppt’.