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

/hets/doc/
H A Dhs2isa.tex24 We present partial translations of Haskell programs to Isabelle that have
25 been implemented as part of the Heterogeneous Tool Set. The the target logic
28 % The AWE package has been used to support a translation of monadic
37 Automating translation from programming languages to the language of a generic
39 verification of programs. It has been argued that functional languages can
40 make the task of proving assertions about programs written in them easier,
41 owing to the relative simplicity of their semantics
42 \cite{Thompson92,Thompson95}. The idea of translating Haskell programs, came
43 to us, more specifically, from an interest in the use of functional languages
44 for the specification of reactiv
[all...]
H A Dcollected_proposals.tex21 also tries to propose how to solve these issues. Most of these
24 which was not thought of during the development of \CASL and its
27 \section{Labels of instantiated formulas}
31 parametrised specifications point to different instantiations of these
39 op symbols in the signature of parameter specifications with their
65 \section{Quick indexing of (all) symbols in a theory}
70 complete mapping of all distinct ids of sorts, preds and / or ops to
76 symbol mappings of translation
[all...]
H A DUserGuide.tex97 %%%%% end of Klaus macros
149 The central idea of the Heterogeneous Tool Set (\protect\Hets) is to
151 integration and proof management. One can think of \Hets acting like a
158 a number of expansion cards (e.g., the theorem provers Isabelle, SPASS
159 and more, as well as model finders). Hence, a variety of tools is
169 \Hets supports a number of input languages directly, such as \CASL,
173 constructs of
177 combination of specification written in different logics.
179 Fig.~\ref{fig:lang} for a simple subset of the
181 specifications or modules written in a specific logic. The graph of
[all...]
/hets/GUI/doc/
H A DWebInterfaceBuildGuide.tex14 This part gives only a very rough overview of what you need.
15 \subsection{Installation of WASH}
28 \subsection{Compilation of hets.cgi}
35 \subsection{Installation of WASH}
57 \subsection{Configuration and Compilation of hets.cgi}
59 All the configuration of the web interface is done via String
/hets/CspCASL/Grammar/
H A DCSP_CASL_Parser.tex47 This is the documentation for the {\sc Csp-Casl} parser. A detailed documentation of the {\sc Csp-Casl} language can be found at:
51 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}.
52 Consequently, the directory containing the {\sc Csp-Casl} parser has to be a direct subdirectory of {\tt Hets}. No special characters
59 \item The newest version of {\bf ghc} has to be correctly installed (currently version is 5.04.2).\\
82 \section{Structure of source files}
86 {\sc Csp-Casl} depends primary on {\sc Casl}, which depends on many other sources of {\tt Hets}. For detailed information about {\sc Casl}, you can find the documentation here:
/hets/Maude/doc/
H A Ddg.tex19 no local axioms and stands for the free models of the theory.
23 The model class of parameterized modules
24 consists of free extensions of the models of their parameters, that are
25 persistent on sorts, but not on kinds. This notion of freeness has been
26 studied in \cite{BouhoulaJouannaudMeseguer00} under assumptions like existence of top sorts for kinds
43 The summation of the module expressions $\mathit{ME}_1$ and
46 the union of the information in both summands. A definition link
66 the current node and the node standing for the free semantics of th
[all...]
/hets/utils/el/
H A Dcasl-indent.el10 (require 'cl) ;need defs of push and pop
18 "*Indentation of casl statements with respect to containing block."
27 (defsubst casl-indent-get-beg-of-line (&optional arg)
29 (beginning-of-line arg)
32 (defsubst casl-indent-get-end-of-line (&optional arg)
34 (end-of-line arg)
38 "Returns the column number of APOINT."
48 of a line.")
58 ;;; customizations for different kinds of environments
96 ;;; redefinition of som
[all...]
/hets/OWL2/java/lib/
H A Dguava-18.0.jarMETA-INF/MANIFEST.MF META-INF/ META-INF/maven/ META-INF/maven/com. ...
/hets/CASL/Termination/
H A DAProVE.jarMETA-INF/ META-INF/MANIFEST.MF aprove/ aprove/CommandLineInterface/ aprove/Framework/ aprove/Framework/Algebra/ aprove/Framework/ ...

Completed in 19 milliseconds