NAME

       cafeobj - algebraic specification and programming language

SYNOPSIS

       cafeobj [OPTION]... [FILES]...

DESCRIPTION

       Starts the CafeOBJ interpreter.

       CafeOBJ  is  a  most  advanced  formal specification language which inherits many advanced
       features (e.g. flexible mix-fix syntax, powerful and  clear  typing  system  with  ordered
       sorts,  parameteric  modules  and  views  for  instantiating  the  parameters,  and module
       expressions, etc.) from OBJ (or more exactly OBJ3) algebraic specification language.

       CafeOBJ is a language for writing formal (i.e. mathematical) specifications of models  for
       wide  varieties  of  software  and  systems,  and  verifying  properties  of them. CafeOBJ
       implements equational logic by rewriting and can be used as a powerful interactive theorem
       proving  system.  Specifiers  can  write  proof scores also in CafeOBJ and doing proofs by
       executing the proof scores.

       CafeOBJ has state-of-art rigorous logical semantics based  on  institutions.  The  CafeOBJ
       cube  shows  the structure of the various logics underlying the combination of the various
       paradigms implemented by  the  language.  Proof  scores  in  CafeOBJ  are  also  based  on
       institution based rigorous semantics, and can be constructed using a complete set of proof
       rules.

OPTIONS

       There are two classes of options. The first are options for  the  cafeobj  wrapper  script
       that  allows  to  select the underlying Common Lisp interpreter, and to adjust search path
       parameters.

       -engine NAME
              selects the underlying common lisp engine. If not given,  the  first  one  selected
              during build time is used.

       -list-engines
              lists all available common lisp engines

       -wrapper-libpath PATH
              sets the path where memory dumps of the lisp interpreters are found

       -wrapper-sharepath PATH
              sets the path where CafeOBJ initialization files are searched

       The following set of options are directed at the CafeOBJ interpreter directly:

       -help  print a help message

       -q     do not load user's initialization file

       -batch run in batch mode

       -p PATH
              gives the standard prelude file defining modules

       +p PATH
              load additional prelude file

       -l DIR-LIST
              set list of pathnames for module search path, separated by colons

       +l DIR-LIST
              adds a list of pathname for module search path

       FILES  files that are loaded at startup time in order.

AUTHOR

       Toshimi Sawada and Norbert Preining.
       Contact: info@cafeobj.org

COPYRIGHT

       Copyright © 2000-2014 Toshima Sawada, Norbert Preining.  License BSD.
       THIS  SOFTWARE  IS SUPPLIED COMPLETELY "AS IS". CafeOBJ is distributed in the hope that it
       will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty  of  MERCHANT-
       ABILITY of FITNESS FOR A PARTICULAR PURPOSE.