Hi Norrathep,
Indeed, the AutoCorres quick-start tutorial assumes a certain degree of familiarity with Isabelle/HOL. To gain some familiarity, I would recommend working through at least the first few chapters of this book by Tobias Nipkow and Gerwin Klein:
http://www.concrete-semantics.org/
Although Isabelle/HOL can be run in batch mode to check proofs, it is primarily an interactive tool. AutoCorres, and also the C parser on which it builds, have not been designed to write specifications and proofs to files. Rather, specifications and proofs are constructed in the internal state of Isabelle/HOL, and the only realistic way to inspect these is in interactive mode.
For example, the following sequence of commands should give you an interactive session looking at the AutoCorres "plus" example:
# Check out l4v and its companion repositories.
# Requires the Google `repo` tool.
# See https://github.com/seL4/verification-manifest/blob/master/README.md for more details.
$ mkdir verification
$ cd verification
$ repo init -u ssh://git@github.com/seL4/verification-manifest.git
$ repo sync
# Build some prerequisites. Requires the "MLton" Standard ML compiler, and possibly some other tools installed.
$ cd l4v
$ make -C tools/c-parser CParser
$ make -C tools/autocorres AutoCorres tests/ROOT
# Start an interactive session.
# Ignore the warnings in the pop-up dialog.
$ ./isabelle/bin/isabelle jedit -d . -l AutoCorres tools/autocorres/tests/examples/Plus.thy &
To see the specifications and definitions produced by the C parser and AutoCorres in the interactive session, make sure you have the "Output" pane open, and type the command "print_theorems" immediately after each of the "install_C_file" and "autocorres" commands, respectively.
Best regards,
Matthew Brecknell
________________________________
From: Devel