Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity
577 Commits 15 Branches 10 Tags 77 MiB
Commit Graph

240 Commits

Author SHA1 Message Date
Achim D. Brucker 459538a1b7 Figure group. 2018-12-04 06:05:49 +00:00
Achim D. Brucker 0f2dc58f5a Multi-file setup. 2018-12-04 05:31:45 +00:00
Burkhart Wolff 17c66f0fea Integrated is_monitor flag for monitor class invariants. 
Makes special treatment of monitor class invariants
possible, when changes of trace are indirect...
 2018-12-03 22:36:08 +01:00
Burkhart Wolff ac1180b529 - checking class invariants 
- checking monitor class invariants
 2018-12-03 22:18:47 +01:00
Burkhart Wolff 9c0bcd86c6 rearrangement 2018-12-03 16:48:15 +01:00
Burkhart Wolff dd942cfb99 rearrangement 2018-12-03 16:46:11 +01:00
Burkhart Wolff 04f5e99e41 First running example for class invariants. 2018-12-03 16:43:27 +01:00
Burkhart Wolff 184a17f977 Refinement: class invariants now gets also the oid from its context. 2018-12-03 14:25:04 +01:00
Burkhart Wolff 6b85bd74cd Very first example of class invariant checking ... 2018-12-03 14:14:53 +01:00
Burkhart Wolff 23bc75d08d Corrections in ontologies (revealed by examples) 
- identified problem: accept/reject conflicts were only detected at application
  time, not at declaration time :-( (leaved as "known problem" for the moment)
- new functionality for declaring doc class invariants
 2018-12-03 13:19:31 +01:00
Burkhart Wolff cf31ffd68b revisions of scholarly paper and report ontologies 2018-11-28 10:49:35 +01:00
Achim D. Brucker 25c295dd7f Merge branch 'master' of logicalhacking.com:HOL-OCL/Isabelle_DOF 2018-11-27 14:22:19 +00:00
Achim D. Brucker 0b79c21d23 Upated title. 2018-11-27 14:18:54 +00:00
Achim D. Brucker d0d5567fc6 Restrucuring. 2018-11-27 13:51:12 +00:00
Achim D. Brucker 1f2551d683 Restrucuring. 2018-11-27 13:39:54 +00:00
Achim D. Brucker 21d51e7275 Restrucuring. 2018-11-27 13:22:31 +00:00
Achim D. Brucker 9d5bddea7c Restrucuring. 2018-11-27 13:11:54 +00:00
Achim D. Brucker b7e39f7d27 Initial commit. 2018-11-27 12:56:42 +00:00
Achim D. Brucker c32425a334 Added note about the state of the document. 2018-11-27 11:34:03 +00:00
Burkhart Wolff 8628ca81ab kleinkram 2018-11-27 11:13:49 +01:00
Achim D. Brucker bfdb5e5260 Restrucuring. 2018-11-27 09:41:04 +00:00
Achim D. Brucker eddc01e1c9 Cleanup. 2018-11-27 09:40:44 +00:00
Achim D. Brucker 0bc6f5521e Restrucuring. 2018-11-27 09:26:54 +00:00
Burkhart Wolff eea65018d1 Rearrangement of the group of TR examples. 
(following structure of math_exams)
 2018-11-21 11:15:21 +01:00
Burkhart Wolff 90f6c2d4ab - New checks for reject sets 
- basic infrastructure for class invariants
 2018-11-20 10:11:11 +01:00
Burkhart Wolff d406b3daeb implemented reject alphabets. (untested) 
slight corrections in MyCommentedIsabelle (MCI)
 2018-11-19 20:53:59 +01:00
Burkhart Wolff 0617315fb0 Small improvements on the term chapter of CommentedIsabelle 2018-11-19 11:32:22 +01:00
Burkhart Wolff f1eabf506c Changed the introduction of MyCommentedIsabelle 2018-11-15 15:20:22 +01:00
Burkhart Wolff 49d49cfcc4 New description of the goal package in the example (I had spare time in my FIIL exam). 2018-11-14 16:33:51 +01:00
Burkhart Wolff 256b2cac56 Exporting the .pdf version from the git-site: 2018-11-13 18:48:21 +01:00
Burkhart Wolff dcda1cc214 Introduced Syntax accept / reject. 
added some semantic for it (incomplete)
some elements on myCommentedIsabelle
 2018-11-13 15:19:02 +01:00
Burkhart Wolff 3a3e99ce98 Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF 2018-11-08 11:08:34 +01:00
Burkhart Wolff 027c501c0d Slight rearrangement in MyCommented. After some comments of readers. 2018-11-08 11:07:41 +01:00
Achim D. Brucker ea1480aecc Re-enabled use of side_by_side_figure. 2018-11-07 22:28:56 +00:00
Burkhart Wolff dd35fa356a Added new TR for MyCommentedIsabelle; many textual corrections. 2018-11-07 22:41:11 +01:00
Burkhart Wolff 18b8e35380 This and that. 2018-11-07 22:37:31 +01:00
Burkhart Wolff fe09c77b89 Moved MyCommentedIsabelle into the example/TR_my_commented isabelle 
- added build structure
- corrected LaTeX
- ... works as a first shot TR !!!
 2018-11-07 15:55:01 +01:00
Burkhart Wolff 3e6dc80445 - experiments with document ontologies 
- substantially more input on "MyCommentedIsabelle"
  (should be another TR example ? )
 2018-11-07 06:00:01 +01:00
Burkhart Wolff 8e216c02f2 wdfs 2018-11-06 11:05:11 +01:00
Achim D. Brucker 46c51235e3 Based all examples on session 'Functional-Automata'. 2018-11-06 09:31:01 +00:00
Achim D. Brucker ab3ba421c8 Fixed ROOT (removed dependency on non-existing ontology.tex. 2018-11-06 09:30:18 +00:00
Achim D. Brucker 4aa8730762 Updated ROOT(s) setup to include AFP entries ... 2018-11-06 09:10:11 +00:00
Burkhart Wolff 9494c05593 - Improved automata-management 
- automata transformation integrated
- control option strict_checking added
- rudimentary tests in IsaDofApplications and Monitor_Example
 2018-11-05 21:42:36 +01:00
Burkhart Wolff 8d9e6cdc48 Big Bang: Restructuring the RegExp Interface, pushing it underneath Isa_DOF, factoring out example into Monitor Example. 2018-11-04 19:15:22 +01:00
Burkhart Wolff 36fac27d0c New Config for 2017 including AFP contributions for Regular-Sets and Regular Automata. 
Added a thin layer interfacing these two.
Slight textual improvements of examples (updates to more recent notations).
 2018-10-30 15:50:01 +01:00
Achim D. Brucker c7665d4dd0 Promoted sections to chapters ... 2018-10-30 01:29:53 +00:00
Achim D. Brucker 55e8f84c77 Switched to technical report. 2018-10-30 00:59:47 +00:00
Achim D. Brucker c05bedf098 Initial setup. 2018-10-30 00:58:45 +00:00
Achim D. Brucker f69d388c49 Updated template. 2018-10-30 00:52:40 +00:00
Achim D. Brucker 862d487b90 Cleanup. 2018-10-30 00:27:07 +00:00
Achim D. Brucker 2923e996f8 Minor layout fixes. 2018-10-29 23:33:21 +00:00
Burkhart Wolff 58f2bff319 no message 2018-10-17 12:31:17 +02:00
Burkhart Wolff df4cf56958 Polish 2018-10-17 12:30:11 +02:00
Burkhart Wolff f1783538bd Cleanup with examples. More commendation. 
Another monitor example added (Concept_Example).
 2018-10-17 12:22:25 +02:00
Burkhart Wolff 0de079cfbb Special ML antiquotation for the trace attribute (a cleaned up version). 2018-10-16 12:23:36 +02:00
Burkhart Wolff 93074bf24d Trace-Calculation refined. One gets the additional information WHICH oid of which class 
is added to the trace.
 2018-10-16 10:44:59 +02:00
Burkhart Wolff 50ff554d53 Typo - correction 2018-10-11 14:55:57 +02:00
Burkhart Wolff 71a889ee58 Automatic trace attribute calculation works on both Attribute and IsaDofApplications. 2018-10-11 13:38:32 +02:00
Burkhart Wolff b220233373 doc_item creation detects enabled monitors … 2018-10-09 15:56:17 +02:00
Burkhart Wolff 8b6a1af99d Kleine Reparaturen hier und da, 
IsaDofApplications Paper weiter “Markupified”.
 2018-10-09 11:59:21 +02:00
Burkhart Wolff 2c80ff8d0a Substantial progress with monitors. 
- infra-structure open_monitor_tab
- computing of enabled ness
- semantics behind open and close monitor.
 2018-10-08 15:13:47 +02:00
Burkhart Wolff 04a354f10a Diverse Code-Massagen/Restruktorationen um Monitore vorzubereiten. 2018-10-08 10:30:53 +02:00
Burkhart Wolff b1e4e64e19 Global revision of the Isa_DOF state - representation as record. 
(Since more components are to come …)
Global revision of the entire example suite.
 2018-10-05 09:45:24 +02:00
Burkhart Wolff b17110db7c comment inside meta_args problem solved. 2018-10-04 17:25:45 +02:00
Burkhart Wolff eaca1959ce Intermediate status : some spacing works. 2018-10-04 16:58:09 +02:00
Burkhart Wolff ac835ea028 First experiments with a more liberal LaTeX parser for meta-args. 2018-10-04 15:58:20 +02:00
Burkhart Wolff e4bb874d86 More markdown in the IsaDofApplications example. 
The new setup is now checked on a Mac for the first time.
 2018-10-02 10:28:24 +02:00
Achim D. Brucker 61d69394c3 Merge branch 'master' of logicalhacking.com:HOL-OCL/Isabelle_DOF 2018-10-02 08:14:23 +01:00
Achim D. Brucker 30e067ec0e Added types. 2018-10-02 08:08:47 +01:00
Achim D. Brucker 484637d83c Removed Text*. 2018-10-02 00:35:50 +01:00
Achim D. Brucker 910f81768f Build script that only copies style files into generation directory. 2018-09-18 17:18:15 +01:00
Achim D. Brucker 4c9c0a2bd1 Changed type of figure width to integer. 2018-09-18 15:34:33 +01:00
Achim D. Brucker 7d5d8590c2 Cleanup. 2018-09-18 14:34:14 +01:00
Achim D. Brucker da7f286dd5 Removed scala converter. 2018-09-18 14:24:25 +01:00
Burkhart Wolff 7d3ecbdefe Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF 
Added stronger example show-case : a “association class” -like Link involving sub-typing.
 2018-09-18 08:57:53 +02:00
Achim D. Brucker 9c042361dd Removed white spaces in *-commands (workaround for bug in Isa_Dof. 2018-09-17 20:30:19 +01:00
Burkhart Wolff 9ef1185add Commenting the InnerSyntaxAntiquotqtion sample. 
This Feature is complete for the moment .
 2018-09-17 17:16:11 +02:00
Burkhart Wolff 7847f1cf01 Cleanup of file “InnerSyntaxAntiquotations”. 2018-09-17 16:58:38 +02:00
Burkhart Wolff 385af317f3 Added appropriate type-checking for ISA docitems as well as another syntax docitem text antiquotation. 2018-09-17 16:48:05 +02:00
Burkhart Wolff 2e097e6b3c rough, non-functional implementation of ISA docitem 2018-09-11 14:15:11 +02:00
Burkhart Wolff 3a44b83ab9 Added new ISA’s and tests. Slight cleanup. 2018-09-11 13:51:25 +02:00
Burkhart Wolff 5eebf2ef5b some more isa’s 2018-09-11 12:08:25 +02:00
Burkhart Wolff f5117da8cb Achim & bu session on LaTeX Gen. 2018-09-11 11:35:25 +02:00
Burkhart Wolff e07b57dd95 Achim/Bu Telco debug. 2018-09-11 09:33:17 +02:00
Burkhart Wolff 0331c5dcbd Cleanup for the ISA infrastructure. 
Checking some Examples.
 2018-09-11 08:50:51 +02:00
Burkhart Wolff bb9c5a4f24 First version with inner-syntax checking infrastructure with just 
one inner syntax antiquotation: file.

Works on some examples.
 2018-09-06 12:07:37 +02:00
Burkhart Wolff d7794e06ac Added ISA_tables (inner syntax antiquotations) 
- Kleinkram.
 2018-09-03 20:56:08 +02:00
Burkhart Wolff 745b335033 small steps here and there 2018-08-30 12:53:02 +02:00
Burkhart Wolff b6b94da82f slight cleanup. 2018-08-28 12:48:07 +02:00
Burkhart Wolff 86e145f723 - restructuring in IsaDOF : 
factoring out create_and_check_docitem
- correction IsaDofApplication
  side_by_side figure commented in and works.
- reaactivated open_monitor.
- changing types of monitor traces : simpler calculation now,
  but more obscure type
- first simulation of monitor trace construction.
 2018-08-27 14:39:34 +02:00
Burkhart Wolff 466552a3d7 - debugging calculations for mutated text items 
- cleanup
- a wee bit serious testing in Attributes.thy
  of this feature.
 2018-08-24 21:57:16 +02:00
Burkhart Wolff 0f36e8b761 Milestone reached: 
- further debugging
- all tests checked
- all examples running (after updates to current attribute conventions)
 2018-08-24 17:14:39 +02:00
Burkhart Wolff 25bcc030b4 Integrated new attribute calculation machinery. 
Sort of works, but problems with inheritance.
Downward incompatibility:
only either long-names or short names allowed for attributes,
but nothing in between.
 2018-08-24 15:49:13 +02:00
Burkhart Wolff 8fcc67978c Resolved the type inference riddle and worked out 
a solution (type matching and instantiation.)
Documented the interface to the type interface
in MyCommentedIsabelle with an example.
 2018-08-22 22:06:15 +02:00
Burkhart Wolff 7f032c439e Cleanups. 
Test environment for attribute evaluations.
 2018-08-18 14:44:39 +02:00
Burkhart Wolff b56c02cd6a Repaired bug in the meta-args parser. 
LaTeX generation for Text* environments with
antiquotation expansion works for the first time.
 2018-08-17 13:19:12 +02:00
Burkhart Wolff 1358540a62 Simplified thy_output (cleanup) and set first LaTeX meta-args generator. 
Restructuring
 2018-08-16 16:52:08 +02:00
Burkhart Wolff 0f12eb2e21 New configuration with modified Isabelle-LaTeX generator. 
Possesses Hook in order to parse meta attributes (not set so far,
default no-parse to empty string).
Current config compiles IsaDofApplications except Text*.
 2018-08-12 08:58:21 +02:00
Burkhart Wolff e81427061b Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF 2018-07-12 12:09:24 +01:00
Burkhart Wolff a07900bfab Some intermediate Hack to find a solution of the text* problem. 
textbis does both interactive and basically correct LaTeX generation
with antiquotation expansion.

At least a thing to study.

bu
 2018-07-12 12:08:58 +01:00