Searched defs:and (Results 1 - 10 of 10) sorted by relevance

/hets/doc/
H A DUserGuideCommonLogic.tex10 \usepackage{charter} % very clean and readable font
26 \usepackage{lstsemantic} % loads listings and defines some languages
52 %% following the points (and some others in the text):
172 used as function or predicate, and \item sequence markers allow
183 like SPASS, darwin and Vampire, such that logical consequences
186 and Leo-II in order to perform induction proofs in theories
204 \section{The Heterogeneous Tool Set and Its Input Languages}
207 provide a general framework for formal methods integration and proof
210 being individual logics (with their analysis and proof tools) as well
213 and mor
[all...]
H A Dhs2isa.tex12 \author{ Paolo Torrini\inst{1} \and
18 \and DFKI Lab Bremen, {\tt \{Christoph.Lueth,Christian.Maeder,Till.Mossakowski\}@dfki.de} }
26 is Isabelle/HOLCF, and the translation is based on a shallow embedding
38 prover may provide useful support for the formal development and the
46 constructor classes, and a syntax for side effects and pseudo-imperative code
55 libraries and efficient automation. Isabelle/HOLCF \cite{holcf}
64 application designed to support heterogeneous specification and the
65 formal development of programs. It has an interface with Isabelle, and
66 relies on Programatica \cite{Prog04} for parsing and stati
[all...]
H A DUserGuide.tex34 %% following the points (and some others in the text):
151 integration and proof management. One can think of \Hets acting like a
153 expansion cards here being individual logics (with their analysis and
154 proof tools) as well as logic translations. Individual logics and
155 their analysis and proof tools can be plugged into the \Hets
159 and more, as well as model finders). Hence, a variety of tools is
166 \caption{The \Hets motherboard and some expansion cards}
170 Common Logic, OWL 2, LF, THF, HOL, Haskell, and Maude. For heterogeneous
175 (if they are formalised as institutions and plugged into
182 currently supported logics and logi
[all...]
/hets/CspCASL/Grammar/
H A DCSP_CASL_Parser.tex51 The {\sc Csp-Casl} parser is being programmed as a part of {\tt Hets} and uses relative paths within the directory structure of {\tt Hets}.
60 {\bf GNU make}, {\tt /usr/local/bin/perl} and {\tt /usr/local/bin/bash} are required, too.
63 \item '{\tt make distclean}' for Linux and '{\tt gmake distclean}' for Solaris users to clean up, then
64 \item '{\tt make hets} ' for Linux and '{\tt gmake hets}' for Solaris users to generate needed\\
66 \item '{\tt cd CspCASL}' and call the script '{\tt ghc-call}', which calls {\bf ghc} with the needed options.
70 \section{Usage and testing}
100 {\bf Parse\_hugo.hs} top-level parsers for basic and named {\sc Csp-Casl}-specs\\
103 {\bf CCToken.hs} Parser for reserved keywords, var and channelName, supports for the top-level parsers
/hets/GUI/doc/
H A DWebInterfaceBuildGuide.tex29 If you want different locations for the generated files and html-links
30 you have to change \verb|HetCATS/GUI/hets_cgi.hs| and then just run
36 All the additionally needed files and patches are in the archive
52 and you end up with \verb|$HOME/wash-pkg/|% $ where the file
53 \verb|package.conf|, all \verb|*.hi|-files and the needed library
57 \subsection{Configuration and Compilation of hets.cgi}
63 After checking and/or changing the configuration constants run
/hets/HasCASL/doc/
H A DStaticAna.tex8 \title{The HasCASL language and its analysis}
19 The HasCASL parser reuses the token (in \texttt{HToken.hs}) and
21 as ids and annotations from the \texttt{Common} directory.
23 The abstract and concrete syntax of HasCASL are given in the summary
26 constructors) for different representation before and after the static
29 (and not on any global information).
34 order -- kinds, types and terms, where predicate types and formulas are
35 special cases of types and terms respectively.
38 constructors and term
[all...]
/hets/utils/el/
H A Dcasl-indent.el10 (require 'cl) ;need defs of push and pop
80 (if (and indent-info (equal tmp (car indent-info)))
136 (defun casl-indent-skip-blanks-and-newlines-forward (end)
137 "Skips forward blanks, tabs and newlines until END."
141 (defun casl-indent-skip-blanks-and-newlines-backward (start)
142 "Skips backward blanks, tabs and newlines upto START."
160 (while (and (not (casl-indent-empty-line-p))
167 (while (and (casl-indent-in-comment start-code (point))
169 (casl-indent-skip-blanks-and-newlines-forward save-point)
174 "If any structure (list or tuple) is not closed, between START and EN
[all...]
/hets/OWL2/java/lib/
H A Dguava-18.0.jarMETA-INF/MANIFEST.MF META-INF/ META-INF/maven/ META-INF/maven/com. ...
H A Dowlapi-osgidistribution-3.5.2.jarMETA-INF/MANIFEST.MF META-INF/ META-INF/maven/ META-INF/maven/net. ...
/hets/CASL/Termination/
H A DAProVE.jarMETA-INF/ META-INF/MANIFEST.MF aprove/ aprove/CommandLineInterface/ aprove/Framework/ aprove/Framework/Algebra/ aprove/Framework/ ...

Completed in 70 milliseconds