-
Notifications
You must be signed in to change notification settings - Fork 19
/
Copy pathUserGuide.tex
2172 lines (1848 loc) · 88.6 KB
/
UserGuide.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
\documentclass{article}
\usepackage[hide]{ed} % set to hide for producing a released version
\usepackage{alltt}
\usepackage{casl}
\usepackage{xspace}
\usepackage{color}
\usepackage{url}
\usepackage{threeparttable,hhline}
\usepackage{paralist}
\usepackage[pdfborder=0 0 0,bookmarks,
pdfauthor={Till Mossakowski, Christian Maeder, Mihai Codescu},
pdftitle={Hets User Guide}]
{hyperref} %% do not load more packages after this line!!
\input{xy}
\xyoption{v2}
\newcommand{\QUERY}[1]%{}
{\marginpar{\raggedright\hspace{0pt}\small #1\\~}}
\newcommand{\eat}[1]{}
\newenvironment{EXAMPLE}[1][] {\par#1\begin{EXAMPLEFORMAT}\begin{ITEMS}}
{\end{ITEMS}\end{EXAMPLEFORMAT}\par}
\newcommand{\IEXT}[1] {\\#1\I}
\newcommand{\IEND} {\I\END}
\newenvironment{EXAMPLEFORMAT} {}{}
%% Added by MB to have some extra vertical space after the ``main'' examples
%% following the points (and some others in the text):
\newenvironment{BIGEXAMPLE} {\begin{EXAMPLE}} {\end{EXAMPLE}\medskip}
\newenvironment{DETAILS}[1][] {#1\begin{DETAILSFORMAT}}{\end{DETAILSFORMAT}}
\newenvironment{DETAILSFORMAT} {}{}
\newenvironment{META}[1][] {#1\begin{METAFORMAT}}{\end{METAFORMAT}}
\newenvironment{METAFORMAT} {\medskip\vrule\hspace{1ex}\vrule\hspace{1ex}%
\begin{minipage}{0.9\textwidth}\it}
{\end{minipage}\par\medskip}
\newcommand{\SLIDESMALL} {}
\newcommand{\SLIDESONLY}[1] {}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% SIMULATING SMALL-CAPS FOR BOLD, EMPH
\newcommand{\normalTEXTSC}[2]{{#1\scriptsize#2}}
%% NOT \newcommand{\normalTEXTSC}[2]{{\normalsize#1\scriptsize#2}}
\newcommand{\largeTEXTSC} [2]{{\large #1\small #2}}
\newcommand{\LargeTEXTSC} [2]{{\Large #1\normalsize#2}}
\newcommand{\LARGETEXTSC} [2]{{\LARGE #1\large #2}}
\newcommand{\hugeTEXTSC} [2]{{\huge #1\Large #2}}
\newcommand{\HugeTEXTSC} [2]{{\Huge #1\LARGE #2}}
%\newcommand {\CASL}{\normalTEXTSC{C}{ASL}\xspace}
\newcommand{\largeCASL} {\largeTEXTSC{C}{ASL}\xspace}
\newcommand{\LargeCASL} {\LargeTEXTSC{C}{ASL}\xspace}
\newcommand{\LARGECASL} {\LARGETEXTSC{C}{ASL}\xspace}
\newcommand {\hugeCASL} {\hugeTEXTSC{C}{ASL}\xspace}
\newcommand {\HugeCASL} {\HugeTEXTSC{C}{ASL}\xspace}
%\newcommand {\CoFI}{CoFI\xspace}
\newcommand {\MAYA}{\normalTEXTSC{M}{AYA}\xspace}
\newcommand{\largeMAYA} {\largeTEXTSC{M}{AYA}\xspace}
\newcommand {\Hets}{\normalTEXTSC{H}{ETS}\xspace}
\newcommand{\largeHets} {\largeTEXTSC{H}{ETS}\xspace}
\newcommand{\LARGEHets} {\LARGETEXTSC{H}{ETS}\xspace}
\newcommand {\Cats}{\normalTEXTSC{C}{ATS}\xspace}
\newcommand{\largeCats} {\largeTEXTSC{C}{ATS}\xspace}
\newcommand {\ELAN}{\normalTEXTSC{E}{LAN}\xspace}
\newcommand{\largeELAN} {\largeTEXTSC{E}{LAN}\xspace}
\newcommand {\HOL}{\normalTEXTSC{H}{OL}\xspace}
\newcommand{\largeHOL} {\largeTEXTSC{H}{OL}\xspace}
\newcommand {\Isabelle}{\normalTEXTSC{I}{SABELLE}\xspace}
\newcommand{\largeIsabelle} {\largeTEXTSC{I}{SABELLE}\xspace}
\newcommand {\SPASS}{\normalTEXTSC{S}{PASS}\xspace}
\newcommand {\Horn}{\normalTEXTSC{H}{ORN}}
%%%%% Klaus macros
\newcommand{\CASLDL}{\textmd{\textsc{Casl-DL}}\xspace}
\newcommand{\Dolce}{\textmd{\textsc{Dolce}}\xspace}
\newcommand{\SHOIN}{$\mathcal{SHOIN}$(\textbf{D})\xspace}
\newcommand{\SROIQ}{$\mathcal{SROIQ}$(\textbf{D})\xspace}
\newcommand{\DL}{DL\xspace}
%%%%% end of Klaus macros
%% Use \ELAN-\CASL, \HOL-\CASL, \Isabelle/\HOL
\newcommand{\LCF}{LCF\xspace}
\newcommand{\ASF}{ASF\xspace}
%%\newcommand {\ASF}{\normalTEXTSC{A}{SF}\xspace}
%%\newcommand{\largeASF} {\largeTEXTSC{A}{SF}\xspace}
\newcommand{\SDF}{SDF\xspace}
%%\newcommand {\SDF}{\normalTEXTSC{S}{DF}\xspace}
%%\newcommand{\largeSDF} {\largeTEXTSC{S}{DF}\xspace}
\newcommand {\ASFSDF}{\normalTEXTSC{A}{SF}+\normalTEXTSC{S}{DF}\xspace}
\newcommand{\largeASFSDF} {\largeTEXTSC{A}{SF}+\largeTEXTSC{S}{DF}\xspace}
\newcommand {\HasCASL}{\normalTEXTSC{H}{AS}\normalTEXTSC{C}{ASL}\xspace}
\newcommand{\largeHasCASL} {\largeTEXTSC{H}{AS}\largeTEXTSC{C}{ASL}\xspace}
%% Do NOT use \ASF+\SDF (it gives a superfluous space in the middle)
\newcommand{\CCC}{CCC\xspace}
\newcommand{\CoCASL}{\normalTEXTSC{C}{O}\normalTEXTSC{C}{ASL}\xspace}
\newcommand{\CspCASL}{\normalTEXTSC{C}{SP}-\normalTEXTSC{C}{ASL}\xspace}
\newcommand{\Csp}{\normalTEXTSC{C}{SP}\xspace}
\newcommand{\CcsCASL}{CCS-\normalTEXTSC{C}{ASL}\xspace}
\newcommand{\CASLLtl}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{L}{TL}\xspace}
\newcommand{\CASLChart}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{C}{HART}\xspace}
\newcommand{\SBCASL}{\normalTEXTSC{S}{B}-\normalTEXTSC{C}{ASL}\xspace}
\newcommand{\HetCASL}{\normalTEXTSC{H}{ET}\normalTEXTSC{C}{ASL}\xspace}
\newcommand{\ModalCASL}{\normalTEXTSC{M}{odal}\normalTEXTSC{C}{ASL}\xspace}
\begin{document}
\title{{\bf \protect{\LARGEHets} User Guide}\\
-- Version 0.99 --}
\author{Till Mossakowski, Christian Maeder,
Mihai Codescu\\[1em]
DFKI GmbH, Bremen, Germany.\\[1em]
Comments to: hets-users@informatik.uni-bremen.de \\
(the latter needs subscription to the mailing list)
}
\maketitle
\section{Introduction}
The central idea of the Heterogeneous Tool Set (\protect\Hets) is to
provide an open source general framework for formal methods
integration and proof management. One can think of \Hets acting like a
motherboard where different expansion cards can be plugged in, the
expansion cards here being individual logics (with their analysis and
proof tools) as well as logic translations. Individual logics and
their analysis and proof tools can be plugged into the \Hets
motherboard using an object-oriented interface based on institutions
\cite{GoguenBurstall92}. The \Hets motherboard already has plugged in
a number of expansion cards (e.g., the theorem provers Isabelle, SPASS
and more, as well as model finders). Hence, a variety of tools is
available, without the need to hard-wire each tool to the logic at
hand.
\begin{figure}
\begin{center}
\includegraphics[width=0.45\textwidth]{hets-motherboard}
\end{center}
\caption{The \Hets motherboard and some expansion cards}
\end{figure}
\Hets supports a number of input languages directly, such as \CASL,
Common Logic, OWL 2, LF, THF, HOL, Haskell, and Maude. For heterogeneous
specification, \Hets offers the language heterogeneous \CASL.
Heterogeneous \CASL (\HetCASL) generalises the structuring
constructs of
\CASL \cite{CASL-UM,CASL/RefManual} to arbitrary logics
(if they are formalised as institutions and plugged into
the \Hets motherboard), as well as to heterogeneous
combination of specification written in different logics.
See
Fig.~\ref{fig:lang} for a simple subset of the
\HetCASL syntax, where \emph{basic specifications} are unstructured
specifications or modules written in a specific logic. The graph of
currently supported logics and logic translations (the latter are also
called comorphisms) is shown in Fig.~\ref{fig:LogicGraph}, and the
degree of support by \Hets in Fig.~\ref{fig:Languages}.
\begin{figure}[ht]
\centering
{\small
\begin{verbatim}
SPEC ::= BASIC-SPEC
| SPEC then SPEC
| SPEC then %implies SPEC
| SPEC with SYMBOL-MAP
| SPEC with logic ID
DEFINITION ::= logic ID
| spec ID = SPEC end
| view ID : SPEC to SPEC = SYMBOL-MAP end
| view ID : SPEC to SPEC = with logic ID end
LIBRARY = DEFINITION*
\end{verbatim}
}
\caption{Syntax of a simple subset of the heterogeneous
specification language.
\texttt{BASIC-SPEC} and \texttt{SYMBOL-MAP} have a logic
specific syntax, while \texttt{ID} stands for some form of
identifiers.\label{fig:lang}
}
\end{figure}
With \emph{heterogeneous structured specifications}, it is possible to
combine and rename specifications, hide parts thereof, and also
translate them to other logics. \emph{Architectural specifications}
prescribe the structure of implementations. \emph{Specification
libraries} are collections of named structured and architectural
specifications.
\Hets consists of logic-specific tools for the parsing and static
analysis of the different involved logics, as well as a
logic-independent parsing and static analysis tool for structured and
architectural specifications and libraries. The latter of course needs
to call the logic-specific tools whenever a basic specification is
encountered.
\Hets is based on the theory of institutions \cite{GoguenBurstall92},
which formalize the notion of a logic. The theory behind \Hets is laid
out in \cite{Habil}. A short overview of \Hets is given in
\cite{MossakowskiEA06,MossakowskiEtAl07b}.
\section{Logics supported by Hets}
The following list of logics (formalized as so-called institutions
\cite{GoguenBurstall92}) is currently supported by \Hets:
\begin{figure}
\begin{center}
\includegraphics[scale=0.4]{LogicGraph}
\end{center}
\caption{Graph of logics currently supported by \Hets. The more an
ellipse is filled with green, the more stable is the implementation of the logic. Blue indicates a prover-supported logic.}
\label{fig:LogicGraph}
\end{figure}
\begin{figure}
\begin{center}
\begin{tabular}{|l|c|c|c|}\hline
Language & Parser & Static Analysis & Prover \\\hline
\CASL & x & x & - \\\hline
\CoCASL & x & x & - \\\hline
\ModalCASL & x & x & - \\\hline
\HasCASL & x & x & - \\\hline
Haskell & (x) & x & - \\\hline
CspCASL & x & x & - \\\hline
CspCASL\_Trace & - & - & x \\\hline
CspCASL\_Failure & - & - & - \\\hline
CommonLogic & x & x & - \\\hline
Constraint\CASL & x & (x) & - \\\hline
Temporal & x & (x) & - \\\hline
RelScheme & x & (x) & - \\\hline
DFOL & x & (x) & - \\\hline
ExtModal & x & (x) & - \\\hline
LF & x & (x) & - \\\hline
%Structured specifications & x & x & (x) \\\hline
%Architectural specifications & x & x & -\\\hline
\CASLDL & x & - & - \\\hline
DMU & x & - & - \\\hline
FreeCAD & - & x & - \\\hline
OWL 2 & x & x & x \\\hline
Propositional & x & x & x \\\hline
QBF & x & x & x \\\hline
SoftFOL & x & - & x \\\hline
Maude & x & x & - \\\hline
VSE & x & x & x \\\hline
THF & x & x & x \\\hline
\Isabelle & (x) & - & x \\\hline
HolLight & x & x & - \\\hline
Adl & x & x & - \\\hline
Fpl & x & x & - \\\hline
EnCL & x & x & x \\\hline
\end{tabular}
\end{center}
\caption{Current degree of \Hets support for the different languages. Languages without prover can still ``borrow'' provers
via logic translations.\label{fig:Languages}}
\end{figure}
\begin{description}
\item[CASL] extends many sorted first-order logic with partial
functions and subsorting. It also provides induction sentences,
expressing the (free) generation of datatypes.
%It is mainly designed and used for the
%specification of requirements for software systems. But it is also
%used for the specification of \Dolce (Descriptive Ontology for
%Linguistic and Cognitive Engineering), an Upper Ontology for knowledge
%representation. \cite{Gangemi:2002:SOD} Further it is now used to
%specify calculi for time and space.
For more details on \CASL see \cite{CASL/RefManual,CASL-UM}.
%
We have implemented the \CASL logic in such a way that much of the
implementation can be re-used for \CASL extensions as well; this
is achieved via ``holes'' (realized via polymorphic variables) in the
types for signatures, morphisms, abstract syntax etc. This eases
integration of \CASL extensions and keeps the effort of integrating
\CASL extensions quite moderate.
\item[CoCASL] \cite{MossakowskiEA04} is a coalgebraic extension of \CASL,
suited for the specification of process types and reactive systems.
The central proof method is coinduction.
\item[ModalCASL] \cite{ModalCASL}
is an extension of \CASL with multi-modalities and
term modalities. It allows the specification of modal systems with
Kripke's possible worlds semantics. It is also possible to express
certain forms of dynamic logic.
\item[ExtModal] is an extended modal logic, subsuming and replacing ModalCASL.
It features -- apart from multiple modalities and dynamic logic -- also time
(and term) modalities, grading, hybrid modal logic, and the $\mu$-calculus
\cite{Codruta10}. Comorphisms to CASL and THF have been implemented.
\item[HasCASL] is a higher order extension of \CASL allowing
polymorphic datatypes and functions. It is closely related to the
programming language Haskell and allows program constructs being
embedded in the specification.
An overview of \HasCASL is given in \cite{Schroeder:2002:HIS};
the language is summarized in \cite{HasCASL/Summary}, the semantics
in \cite{Schroder05b,Schroder-habil}.
\item[Haskell] is a modern, pure and strongly typed functional programming
language. With various language extensions it simultaneously is the
implementation language of \Hets. As a logic we only supports the older
Haskell 98 standard. Yet, in principle, \Hets might be applied to itself --
in some more distant future. The definitive reference for Haskell is
\cite{PeytonJones03}, see also \url{www.haskell.org}.
\item[CspCASL] \cite{Roggenbach06} is a combination of \CASL
with the process algebra \Csp.
\item[CommonLogic] \url{http://en.wikipedia.org/wiki/Common_logic}
\item[ConstraintCASL] is an experimental logic for the specification
of qualitative constraint calculi.
\item[OWL 2] is the Web Ontology Language (OWL 2) recommended by the
World Wide Web Consortium (W3C, \url{http://www.w3c.org}). It is
used for knowledge representation and the Semantic Web
\cite{berners:2001:SWeb}.
Hets calls an external OWL 2 parser
written in JAVA to obtain the abstract syntax for an OWL file and its
imports. The JAVA parser is also doing a first analysis classifying
the OWL ontology into the sublanguages OWL Full, OWL DL and OWL
Lite.
Hets only supports the last two, more restricted variants.
The
structuring of the OWL imports is displayed as Development Graph.
\item[CASL-DL] \cite{OWL-CASL-WADT2004}
is an extension of a restriction of \CASL, realizing
a strongly typed variant of OWL in \CASL syntax.
It extends
\CASL with cardinality restrictions for the description of sorts and
unary predicates. The restrictions are based on the equivalence
between \CASLDL, OWL and \SHOIN. Compared to \CASL only unary
and binary predicates, predefined datatypes and concepts (subsorts
of the topsort Thing) are allowed. It is used to bring OWL and
\CASL closer together.
\item[Propositional] is classical propositional logic, with
the zChaff SAT solver \cite{Herbstritt03} connected to it.
\item[QBF] are quantified boolean formulas, with
DepQBF \url{http://fmv.jku.at/depqbf/} connected to it.
\item[RelScheme] is a logic for relational databases \cite{DBLP:journals/ao/SchorlemmerK08}.
\item[SoftFOL] \cite{LuettichEA06a} offers several automated theorem
proving (ATP) systems for first-order logic with equality:
\begin{itemize}
\item \SPASS
\cite{WeidenbachEtAl02}, see \url{http://www.spass-prover.org};
\item Vampire \cite{RiazanovV02} see \url{http://www.vprover.org};
\item Darwin \cite{Baumgartner:etal:Darwin:IJAIT:2005}, see \url{http://combination.cs.uiowa.edu/Darwin};
\item Eprover \cite{Schulz:AICOM-2002}, see \url{http://www.eprover.org};
\item E-KRHyper \cite{DBLP:conf/cade/PelzerW07}, see \url{http://www.uni-koblenz.de/~bpelzer/ekrhyper}, and
\item
MathServe Broker\footnote{which chooses an appropriate ATP upon a
classification of the FOL problem} \cite{ZimmerAutexier06}.
\end{itemize}
These together comprise some of the most advanced theorem provers
for first-order logic. SoftFOL is essentially the first-order
interchange language TPTP \cite{DBLP:conf/lpar/Sutcliffe10},
see \url{http://www.tptp.org}.
\item[THF] simply typed lambda calculus, is an interchange language for
(typed) higher-order logic \cite{DBLP:conf/cade/BenzmullerRS08}, similar to
what TPTP is for (untyped) first-order logic. \Hets connects THF to the
automated higher-order provers Leo-II, Satallax and Isabelle's nitpick,
refute and sledgehammer.
\item[\Isabelle] \cite{NipPauWen02} is an interactive theorem prover
for higher-order logic.
\item[HolLight] \url{http://www.cl.cam.ac.uk/~jrh13/hol-light/}
is John Harrison's interactive theorem prover
for higher-order logic.
\item[VSE] is an interactive theorem prover, see \ref{subsec:VSE}.
\item[DMU] is a dummy logic to read output of ``Computer Aided
Three-dimensional Interactive Application'' (Catia).
\item[FreeCAD] is a logic to read design files of the CAD system
FreeCAD\\\url{http://sourceforge.net/projects/free-cad}.
\item[Maude] is a rewrite system \url{http://maude.cs.uiuc.edu/} for
first-order logic. In order to use this logic the environment variable
\verb+HETS_MAUDE_LIB+ must be set to a directory containing the files
\verb+full-maude.maude+, \verb+hets.prj+, \verb+maude2haskell.maude+ and
\verb+parsing.maude+.
\item[DFOL] is an extension of first-order logic with dependent types \cite{rabe:dfol:06}.
\item [LF] is the dependent type theory of Twelf \url{http://twelf.plparty.org/}. Hets
calls Twelf on \verb+.elf+ files (for this, the environment variable
\verb+TWELF_LIB+ must be set) and reads in the OMDoc generated by Twelf.
Moreover, LF can be used as a logical framework to add new logics in Hets \cite{CHK+2011a}.
Logic definitions in LF are based in the logic atlas of the Latin project \cite{project:latin}
and therefore the environment variable \verb+LATIN_LIB+ must be set to the
repository with the Latin logic definitions.
\item[Framework] is a dummy logic added for declarative logic definitions \cite{CHK+2011a}.
\item[Adl] is ``A Description Language'' based on relational algebra originally
designed for requirements engineering of business rules
\url{https://lab.cs.ru.nl/BusinessRules/Requirements_engineering}.
\item[Fpl] is a ``logic for functional programs'' as an extension of a
restriction of \CASL (predicates are disabled) \cite{Sannella12}.
\item[EnCL] is an ``engineering calculation language'' based on first
order theory of real numbers with some predefined binders
\cite{logic:EnCL}. It allows the formulation of executable
specifications of engineering calculation methods. For the execution
of these specifications Hets provides connections to the computer
algebra systems Mathematica, Maple and Reduce.
\end{description}
Various logics are supported with proof tools. Proof support for the
other logics can be obtained by using logic translations to a
prover-supported logic.
An introduction to \CASL can be found in the \CASL User Manual
\cite{CASL-UM}; the detailed language reference is given in
the \CASL Reference Manual \cite{CASL/RefManual}. These documents
explain both the \CASL logic and language of basic specifications as
well as the logic-independent constructs for structured and
architectural specifications. The corresponding document explaining the
\HetCASL language constructs for \emph{heterogeneous} structured specifications
is the \HetCASL language summary \cite{Mossakowski04}; a formal
semantics as well as a user manual with more examples are in preparation.
Some of \HetCASL's heterogeneous constructs will be illustrated
in Sect.~\ref{sec:HetSpec} below.
\section{Logic translations supported
by Hets}
\label{comorphisms}
Logic translations (formalized as institution comorphisms
\cite{GoguenRosu02}) translate from a given source logic to a given
target logic. More precisely, one and the same logic translation
may have several source and target \emph{sub}logics: for
each source sublogic, the corresponding sublogic of the target
logic is indicated.
A graph of the most important logics and sublogics, together with their
comorphisms, is shown in Fig.~\ref{fig:SublogicGraph}.
\begin{figure}
\begin{center}
\includegraphics[scale=0.4]{SublogicGraph}
\end{center}
\caption{Graph of most important sublogics currently supported by \Hets,
together with their comorphisms.}
\label{fig:SublogicGraph}
\end{figure}
In more detail, the following list of logic translations is currently
supported by \Hets:
\begin{tabular}{|l|p{8cm}|}\hline
Adl2CASL & inclusion taking relations to CASL predicates \\\hline
CASL2CoCASL & inclusion \\\hline
CASL2CspCASL & inclusion \\\hline
CASL2HasCASL & inclusion \\\hline
CASL2Isabelle & inclusion on sublogic CFOL=
(translation $(7)$ of \cite{Mossakowski02}) \\\hline
CASL2Modal & inclusion \\\hline
CASL2PCFOL & coding of subsorting (SubPCFOL=) by injections, see Chap.\ III:3.1 of the CASL Reference Manual \cite{CASL/RefManual} \\\hline
CASL2PCFOLTopSort & coding of subsorting (SulPeCFOL=) by a top sort and unary
predicates for the subsorts \\\hline
CASL2Propositional & translation of propositional FOL \\\hline
CASL2SoftFOL & coding of CASL.SuleCFOL=E to SoftFOL \cite{LuettichEA06a},
mapping types to soft types \\\hline
CASL2SoftFOLInduction & same as CASL2SoftFOL but with instances of induction
axioms for all proof goals \\\hline
CASL2SoftFOLInduction2 & similar to CASL2SoftFOLInduction but replaces goals with induction premises \\\hline
CASL2SubCFOL & coding of partial functions by error elements
(translation $(4a')$ of \cite{Mossakowski02}, but extended to subsorting, i.e. sublogic SubPCFOL=) \\\hline
CASL2VSE & inclusion on sublogic CFOL= \\\hline
CASL2VSEImport & inclusion on sublogic CFOL= \\\hline
CASL2VSERefine & refining translation of CASL.CFOL= to VSE \\\hline
CASL\_DL2CASL & inclusion \\\hline
CoCASL2CoPCFOL & coding of subsorting by injections, similar to CASL2PCFOL \\\hline
CoCASL2CoSubCFOL & coding of partial functions by error supersorts, similar to CASL2SubCFOL \\\hline
CoCASL2Isabelle & extended translation similar to CASL2Isabelle \\\hline
CommonLogic2CASL & Coding Common Logic to \CASL.Module elimination
is applied before translating to \CASL. \\\hline
CommonLogic2CASLCompact & Coding compact Common Logic to \CASL.
Compact Common Logic is a sublogic of Common Logic
where no sequence markers occur. Module elimination
is applied before translating to \CASL. We recommend
using this comorphism whenever possible because it
results in simpler specifications.\\\hline
CommonLogicModuleElimination & Eliminating modules from a Common Logic theory
resulting in an equivalent specification without
modules. \\\hline
CspCASL2CspCASL\_Failure & inclusion \\\hline
CspCASL2CspCASL\_Trace & inclusion \\\hline
CspCASL2Modal & translating the CASL data part to ModalCASL \\\hline
DFOL2CASL & translating dependent types \\\hline
DMU2OWL & interpreting Catia output as OWL \\\hline
\end{tabular}
\begin{tabular}{|l|p{7cm}|}\hline
HasCASL2HasCASLNoSubtypes & coding out subtypes \\\hline
HasCASL2HasCASLPrograms & coding of \HasCASL axiomatic recursive definitions
as \HasCASL recursive program definitions \\\hline
HasCASL2Haskell & translation of \HasCASL recursive program definitions to Haskell \\\hline
HasCASL2IsabelleOption & coding of HasCASL to Isabelle/HOL \cite{Groening05} \\\hline
Haskell2Isabelle & coding of Haskell to Isabelle/HOL \cite{TorriniEtAl07} \\\hline
Haskell2IsabelleHOLCF & coding of Haskell to Isabelle/HOLCF \cite{TorriniEtAl07} \\\hline
HolLight2Isabelle & coding of HolLight to Isabelle/HOL \\\hline
Maude2CASL & encoding of rewrites as predicates \\\hline
Modal2CASL & the standard translation of modal logic
to first-order logic \cite{blackburn_p-etal:2001a} \\\hline
OWL2CASL & inclusion \\\hline
OWL2CommonLogic & inclusion \\\hline
Propositional2CASL & inclusion \\\hline
Propositional2QBF & inclusion \\\hline
QBF2Propositional & inclusion \\\hline
RelScheme2CASL & inclusion \\\hline
\end{tabular}
\section{Getting started}
The latest \Hets version can be obtained from the
\Hets tools home page
\begin{quote}
\url{http://www.dfki.de/cps/hets}
\end{quote}
Since \Hets is being
improved constantly, it is recommended always to use the latest version.
\Hets is currently available (on Intel architectures only) for Linux
and with limited functionality for Mac OSX.
There are several possibilities to install \Hets.
\begin{enumerate}
\item
The best support is currently given via Ubuntu packages.
\begin{verbatim}
sudo apt-add-repository ppa:hets/hets
sudo apt-get update
sudo apt-get install hets
\end{verbatim}
This will also install quite a couple of tools for proving requiring about
800 MB of disk space. For a minimal installation \texttt{apt-get install
hets-core} instead of \texttt{hets}.
The following software will be installed, too:
\medskip
{\small
\begin{tabular}{|l|l|p{5cm}|}\hline
Hets-lib & specification library & \url{http://www.cofi.info/Libraries}\\\hline
uDraw(Graph) & graph drawing & \url{http://www.informatik.uni-bremen.de/uDrawGraph/en/}\\\hline
Tcl/Tk & graphics widget system & (version 8.4 or 8.5)\\\hline
\SPASS & theorem prover & \url{http://spass.mpi-sb.mpg.de/}\\\hline
Darwin & theorem prover & \url{http://combination.cs.uiowa.edu/Darwin/}\\\hline
\end{tabular}
}
\medskip
A daily snapshot of \texttt{hets} can be installed by:
\begin{verbatim}
sudo hets -update
\end{verbatim}
In case the binary (under \texttt{/usr/lib/hets/hets}) is broken it can be replaced manually or by reverting an update:
\begin{verbatim}
sudo hets -revert
\end{verbatim}
\item For Mac OSX we provide disk images \texttt{Hets-<date>.dmg} without GTK support.
\item
You may compile \Hets from the sources (they are licensed under GPL),
please follow the
link ``Hets: source code and information for developers''
on the \Hets web page, download the sources (as tarball or from
svn), and follow the
instructions in the \texttt{INSTALL} file, but be prepared to take some time.
\end{enumerate}
Depending on your application further tools are supported and may be
installed in addition:
\medskip
{\small
\begin{tabular}{|l|l|p{5cm}|}\hline
\Isabelle & theorem prover & \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}\\\hline
(X)Emacs & editor (for Isabelle) & \\\hline
zChaff & SAT solver & \url{http://www.princeton.edu/~chaff/zchaff.html} \\\hline
minisat & SAT solver & \url{http://minisat.se/} \\\hline
Pellet & OWL 2 reasoner & \url{http://clarkparsia.com/pellet/} \\\hline
E-KRHyper & theorem prover
& \url{http://userpages.uni-koblenz.de/~bpelzer/ekrhyper/} \\\hline
Reduce & computer algebra system
& \url{http://www.reduce-algebra.com/} \\\hline
Maude & rewrite system & \url{http://maude.cs.uiuc.edu/} \\\hline
VSE & theorem prover & (non-public) \\\hline
Twelf & & \url{http://twelf.plparty.org/} \\\hline
\end{tabular}
}
\section{Analysis of Specifications}
Consider the following \CASL
specification:
\medskip
\begin{BIGEXAMPLE}
\I\SPEC \NAME{Strict\_Partial\_Order} =
%%PDM\I{} \COMMENTENDLINE{Let's start with a simple example !}
\begin{ITEMS}[\PRED]
\I\SORT \( Elem \)
\I\PRED \( \_\_<\_\_ : Elem \* Elem \)
% \COMMENTENDLINE{\PRED abbreviates predicate}
\end{ITEMS}
\(\[ \FORALL x,y,z : Elem \\
\. \NOT(x < x) \RIGHT{\LABEL{strict}} \\
\. x < y \IMPLIES \NOT(y < x) \RIGHT{\LABEL{asymmetric}} \\
\. x < y \A y < z \IMPLIES x < z \RIGHT{\LABEL{transitive}} \\
\]\)
\begin{COMMENT}
Note that there may exist \(x, y\) such that\\
neither \(x < y\) nor \(y < x\).
\end{COMMENT}
\I\END
\end{BIGEXAMPLE}
\Hets can be used for parsing and
checking static well-formedness of specifications.
\index{parsing}%
\index{static!analysis}%
\index{analysis, static}%
Let us assume that the example is in a file named
\texttt{Order.casl} (actually, this file is provided
with the \Hets distribution as \texttt{Hets-lib/UserManual/Chapter3.casl}).
Then you can check the well-formedness of the
specification by typing (into some shell):
\begin{quote}
\texttt{hets Order.casl}
\end{quote}
\Hets checks both the correctness of this specification
with respect to the \CASL syntax, as
well as its correctness with respect to the static semantics (e.g.\
whether all identifiers have been declared before they are used,
whether operators are applied to arguments of the correct sorts,
whether the use of overloaded symbols is unambiguous, and so on).
The following flags are available in this context:
\begin{description}
\item[\texttt{-p}, \texttt{--just-parse}] Just do the parsing
-- the static analysis is skipped and no development is created.
\item[\texttt{-s}, \texttt{--just-structured}] Do the parsing and the
static analysis of (heterogeneous) structured specifications, but
leave out the analysis of basic specifications. This can be used
for prototyping issues, namely to quickly produce a development graph
showing the dependencies among the specifications (cf.
Sect.~\ref{sec:DevGraph}) even if the individual specifications are
not correct yet.
\item[\texttt{-L DIR}, \texttt{--hets-libdir=DIR}]
Use \texttt{DIR} as a colon separated list of directories for specification libraries (equivalently, you can set the variable \texttt{HETS\_LIB} before
calling \Hets).
\item[\texttt{-a ANALYSIS}, \texttt{--casl-amalg=ANALYSIS}]
For the analysis of architectural specification (a quite advanced
feature of \CASL), the \texttt{ANALYSIS} argument specifies the options for
amalgamability checking
algorithm for \CASL logic; it is a comma-separated list of zero or
more of the following options:
\begin{description}
\item[\texttt{sharing}] perform sharing analysis for sorts,
operations and predicates.
\item[\texttt{cell}] perform cell condition check; implies
\texttt{sharing}. With this option on, the subsort embeddings are
analyzed.
\item[\texttt{colimit-thinness}] perform colimit thinness check;
implies \texttt{sharing}. The colimit thinness check is less
complete and usually takes longer than the full cell condition
check (\texttt{cell} option), but may prove more efficient in case
of certain specifications.
\end{description}
If \texttt{ANALYSIS} is empty then amalgamability analysis for
\CASL is skipped.
The default value for \texttt{--casl-amalg} is
\texttt{cell}.
\end{description}
\section{Heterogeneous Specification} \label{sec:HetSpec}
\Hets accepts plain text input files with the following endings:
\\
\begin{tabular}{|l|c|c|}\hline
Ending & default logic & structuring language\\\hline
\texttt{.casl} & \CASL & \CASL \\\hline
\texttt{.het} & \CASL & \CASL \\\hline
\texttt{.hol} & HolLight & HolLight \\\hline
\texttt{.hs} & Haskell & Haskell \\\hline
\texttt{.owl} & OWL 2 & OWL \\\hline
\texttt{.elf} & LF & Twelf \\\hline
\texttt{.clf} or \texttt{.clif} & CommonLogic & \CASL \\\hline
\texttt{.maude} & Maude & Maude \\\hline
\end{tabular}
\medskip
Furthermore, \texttt{.xml} files are accepted as Catia output if the default
logic is set to DMU before a library import or by the ``\texttt{-l DMU}''
command line option of \Hets. In all other cases \texttt{.xml} files are
assumed to be development graph files as produced by ``\texttt{-o xml}''.
Although the endings \texttt{.casl} and \texttt{.het} are
interchangeable, the former should be used for libraries of
homogeneous \CASL specifications and the latter for \HetCASL libraries
of heterogeneous specifications (that use the \CASL structuring
constructs). Within a \HetCASL library, the current logic can be changed e.g.\
to \HasCASL in the following way:
\begin{verbatim}
logic HasCASL
\end{verbatim}
The subsequent specifications are then parsed and analysed as
\HasCASL specifications. Within such specifications,
it is possible to use references to named \CASL specifications;
these are then automatically translated along the default
embedding of \CASL into \HasCASL (cf.\ Fig.~\ref{fig:LogicGraph}).
(There are also heterogeneous constructs
for explicit translations between logics, see \cite{Mossakowski04}.)
\eat{
A \CspCASL specification consists of a \CASL specification
for the data part and a \Csp process built over this data part.
Therefore, \HetCASL provides a heterogeneous language construct
\texttt{data} as follows:
\begin{verbatim}
library Buffer
logic CASL
spec List =
free type List[Elem] ::= nil | cons(Elem; List[Elem])
ops last: List -> ? Elem;
rest: List -> ? List
end
logic CspCASL
spec Buffer =
data List
channel read, write : Elem
process Buf(List): read, write, List;
EmptyBuffer : read,write, List;
Buf(l)= read? x :: Elem -> Buf(cons(x,nil)) []
(if l=nil then STOP else
write!last(l) -> Buf(rest(l)))
EmptyBuffer = Buf(nil)
end
\end{verbatim}
Here, the construct \texttt{data List} refers to the \CASL specification
\texttt{List}, which is implicitly embedded into \CspCASL.
}
The ending \texttt{.hs} is available for directly reading in
Haskell programs % and HasSLe specifications,
and hence supports the Haskell module system.
By contrast, in \HetCASL libraries (ending with \texttt{.het}),
the logic Haskell has to be chosen explicitly, and the \CASL structuring
syntax needs to be used:
\begin{verbatim}
library Factorial
logic Haskell
spec Factorial =
{
fac :: Int -> Int
fac n = foldl (*) 1 [1..n]
}
end
\end{verbatim}
Note that according to the Haskell syntax, Haskell function
declarations and definitions need to start with the first column of
the text.
\section{Development Graphs}\label{sec:DevGraph}
Development graphs are a simple kernel formalism for (heterogeneous)
structured theorem proving and proof management.
A development graph consists of a set of nodes (corresponding to whole
structured specifications or parts thereof), and a set of arrows
called \emph{definition links}, indicating the dependency of each
involved structured specification on its subparts. Each node is
associated with a signature and some set of local axioms. The axioms
of other nodes are inherited via definition links. Definition links
are usually drawn as black solid arrows, denoting an import of another
specification.
Complementary to definition links, which \emph{define} the theories of
related nodes, \emph{theorem links} serve for \emph{postulating}
relations between different theories. Theorem links are the central
data structure to represent proof obligations arising in formal
developments.
Theorem links can be \emph{global} (drawn as solid arrows) or
\emph{local} (drawn as dashed arrows): a global theorem link
postulates that all axioms of the source node (including the inherited
ones) hold in the target node, while a local theorem link only postulates
that the local axioms of the source node hold in the target node.
Both definition and theorem links can be \emph{homogeneous},
i.e. stay within the same logic, or \emph{heterogeneous}, i.e.\ %% such that
the logic changes along the arrow. Technically, this is the case
for Grothendieck signature morphisms $(\rho,\sigma)$ where
$\rho\not=id$. This case is indicated with double arrows.
Theorem links are initially displayed in red.
The \emph{proof calculus} for development graphs
\cite{MossakowskiEtAl05,Habil} is given by rules
that allow for proving global theorem links by decomposing them
into simpler (local and global) ones. Theorem links that have been
proved with this calculus are drawn in green. Local theorem links can
be proved by turning them into \emph{local proof goals}. The latter
can be discharged using a logic-specific calculus as given by an
entailment system for a specific institution. Open local
proof goals are indicated by marking the corresponding node in the
development graph as red; if all local implications are proved, the
node is turned into green. This implementation ultimately is based
on a theorem \cite{Habil} stating soundness and relative completeness
of the proof calculus for heterogeneous development graphs.
Details can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}
and in \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}.
The following options let \Hets show the development graph of
a specification library:
\begin{description}
\item[\texttt{-g}, \texttt{--gui}] Shows the development graph in a GUI window
\item[\texttt{-u}, \texttt{--uncolored}] no colors in shown graphs
\end{description}
The following additional options also apply typical rules from the development
graph calculus to the final graph and save applying these rule via the GUI.
\begin{description}
\item[\texttt{-A}, \texttt{--apply-automatic-rule}] apply the automatic
strategy to the development graph. This is what you usually want in order to
get goals within nodes for proving.
\item[\texttt{-N}, \texttt{--normal-form}] compute all normal forms for nodes
with incoming hiding links. (This may take long and may not be implemented
for all logics.)
\end{description}
\eat{
Let us extend the above library \texttt{Order.casl}. One use of the
library might be to express the fact that the natural numbers form a
strict partial order as a view, as follows:
\medskip
\begin{BIGEXAMPLE}
\I\SPEC \NAMEREF{Natural} = ~\FREE \TYPE \(Nat ::= 0 \| suc(Nat)\)~\END
\end{BIGEXAMPLE}
\begin{EXAMPLE}
\I\SPEC \NAMEDEFN{Natural\_Order\_2} =
\IEXT{\NAMEREF{Natural}} \THEN
\begin{ITEMS}
\I\PRED \( \_\_<\_\_ : Nat \* Nat\)
\end{ITEMS}
\(\[ \FORALL x,y:Nat \\
\. 0 < suc(x) \\
\. \neg x < 0 \\
\. suc(x) < suc(y) \IFF x < y
\]\)
\I\END
\end{EXAMPLE}
\begin{EXAMPLE}%[\SLIDESMALL]
\I\VIEW \NAMEDEFN{v1} ~:~ \NAMEREF{Strict\_Partial\_Order} \TO
\NAMEREF{Natural\_Order\_2} =
\I{} \( Elem \MAPSTO Nat\)
\I\END
\end{EXAMPLE}
Again, these specifications can be checked with \Hets. However, this
only checks syntactic and static semantic well-formedness -- it is
\emph{not} checked whether the predicate `$\_\_<\_\_$' introduced in
\NAMEREF{Natural\_Order\_2} actually is constrained to be interpreted
by a strict partial ordering relation. Checking this requires theorem
proving, which will be discussed below.
However, before coming to theorem proving, let us first inspect the
proof obligations arising from a specification. This can be done with:
\begin{quote}
\texttt{hets -g Order.casl}
\end{quote}
(assuming that the above two specifications and the view
have been added to the file
\texttt{Order.casl}).
\Hets now displays a so-called development graph
(which is just an overview graph showing the overall structure
of the specifications in the library), see Fig.~\ref{fig:dg0}.
\begin{figure}
\begin{center}
\includegraphics[scale=0.7]{dg-order-0}
\end{center}
\caption{Sample development graph.\label{fig:dg0}}
\end{figure}
Nodes in a development graph correspond to \CASL specifications.
Arrows show how specifications are related by the structuring
constructs.
The black arrow denotes an ordinary import of
specifications (generated by the extension), while the red arrow
denotes a proof obligation (corresponding to the view).
This proof obligation needs to be discharged in order to
show that the view is well-formed (then its color turns into green).
As a more complex example, consider the following loose specification
of a sorting function, taken from the \CASL User Manual
\cite{CASL-UM}, Chap.~6:
\begin{BIGEXAMPLE}
\I\SPEC \NAMEREF{List\_Order\_Sorted}
\\{} [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
\begin{ITEMS}[\WITHIN]
\I\LOCAL
\begin{ITEMS}[\PRED]
\I\PRED \( \_\_is\_sorted : List \)
\end{ITEMS}
\(\[ \FORALL e,e': Elem; L : List \\
\. empty~is\_sorted \\
\. cons(e,empty)~is\_sorted \\
\. cons(e,cons(e',L))~is\_sorted \IFF
\\\M (cons(e',L)~is\_sorted \A \NOT(e'<e)) \]\)
\I\WITHIN
\begin{ITEMS}[\OP]
\I\OP \( order : List \TOTAL List \)
\end{ITEMS}
\( \FORALL L:List\. \[ order(L)~is\_sorted \]\)
\end{ITEMS}
\I\END
\end{BIGEXAMPLE}
The following specification of sorting by insertion also is taken from
the \CASL User Manual \cite{CASL-UM}, Chap.~6:
\begin{BIGEXAMPLE}
\I\SPEC \NAMEREF{List\_Order}
[\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
\phantomsection
\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
\begin{ITEMS}[\WITHIN]