Plan and priority list for CoFI tool activities ************************************************ Christian ************************************************ CASL-Parser mit Parsec statische Analyse von CASL (mit Till) Signatur-Morphismen + Analyse CASL-Instanz der Typklasse Logic Sprachdesign HasCASL Verhältnis von Parametrisierung und Polymorphie/Typklassen (Has)CASL Abstract syntax + signatures in Haskell (Has)CASL-parser in Haskell Static analysis for HasCASL Data types Signatures, Formulas Collection of signature Mixfix-Analysis (via combinator parsing) Type check (see ghc ?), (overload resolution) Symbol map analysis Weak amalgamation analysis Conversion ASF/SDF-Parser -> abstract syntax (in Haskell) Comparsion of parsers (ML-yacc parser, SDF-Parser) Conversion-Tool 1.0 => 1.0.1 komplettieren PVS anbinden (Kooperation mit Cachan?) Encoding for HasCASL in Isabelle/HOL Instantiate Transformation Application system for HasCASL Automatic generation of Haskell (for a HasCASL subset) Proofs in HasCASL Case study Sönke Magnussen kontaktieren (der arbeitet mit Has-CASL-ähnlicher Sprache) arch/arch_types.ml Semantic domains for architectural specs arch/sharing.ml Sharing analysis for architectural specs ************************************************ Klaus ************************************************ Joost Visser wg. ATerms in Haskell => neues Repository Abstrakte Syntax von SML-CATS einlesen LaTeX-Ausgabe Simple logics: Prop(and, or, not) Prop(implies, false) + translations Heterogeneous lexer (comments, " ", \) Heterogeneous parser struct_ana.sml Static analysis of structured specs (mit Till) lib_ana.sml Static analysis of libraries (dto.) Read in SML-CATS-global_env in HetCATS Portations: Intel-Solaris, Mac OS-10 (2 weeks) (X)Emacs mode for CASL, hide Display Annotations (2 weeks) -> Raffael Sturm Views on CASL specs: CATS/viewer.sml (2 weeks) Uebersetzung von CASL-LaTeX-Spezifikationen nach ASCII Module graph CATS/module_graph.sml (1 week) -> Maya? ATerms via XML: CATS/aterms.sml (2 weeks) Web-interface: CATS/web_interface2.sml (1 week) Neues Tool-Schaubild auf Web-Seiten veröffentlichen Library management: CATS/lib_ana.sml (2 weeks) Version management/Uniform Workbench: CATS/lib_ana.sml (2 months) Port Maya to Haskell (x months) arch/arch_analysis.ml Static analysis of architectural specs ************************************************ Pascal ************************************************ XML: CATS/xml/xml_convert.sml ************************************************ Bartek ************************************************ Invoice example: ask Hubert if it now behaves as expected Adapt symbol map analysis to new semantics symmaps/stat_symmaps.ml Adapt architectural analysis to diagram semantics Include line numbers into error messages (cf. basic_ana.sml how to do this) Better error messages when symbol maps are wrong: which is the symbol/raw symbol that causes the problem? Non-final unions: shorten error message: output only one element per equivalence class ************************************************ Markus, Lutz ************************************************ Beweise in Isabelle CASL consistency checker Weitere %implies-Annotationen zu den Basic Datatypes hinzufuegen (Vorbild: Larch-Handbuch) Simpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln Parser and static analysis for CSP-CASL ************************************************ Christoph ************************************************ CASL consistency checker IsaWin: CASL-libraries unterstützen ************************************************ Dieter/Serge ************************************************ Better Syntax interface for Maya Extend Maya to DG with hiding Extend Maya to heterogeneous DGs ************************************************ Till ************************************************ Mark-Oliver Stehr, Hamburg wg. HOL-Nurpl-Translation in Maude Coq, PTT in Maude Proof general interface (1 day) Test Maya with basic datatypes Make static analysis institution independent (WADT01) (2 months) Klärung: davinci oder dot? Fine tuning of parser (comments, compound ids): CATS/CASL.grm (3 days) Abstract syntax: CATS/CASLsign/asgen.sml (1 day) Revise basic analysis: CATS/basic_ana.sml (1 month) Check %implies: CATS/struct_ana.sml (1 day) Extend envs: global_env.sml, CATS/CASLsign/local_env.sml (3 days) Revise type checking: CATS/overload.sml (2 weeks) ID Vergleich als ID1 Vergleich (überall) (1 day) Verbesserung der Fehlermeldungen Improve encoding: CATS/basic_encode.sml (3 days) More HOL-theories: CATS/HOL-CASL/struct_encode.sml (2 days) Renamings in hide-elimination: CATS/struct_encode.sml, CATS//flatten.sml (1 week) Example of Agnes und Frank: proofs in HOL-CASL (2 days) Term input+errors in cmd line interface: CATS/casl/casl.sml (1 day) Examples for cond rewriting -> Christophe Doku: VSE-Prover, VSE-Method VSE-demo in Bremen? Adapt more stuff from isabelle/src/HOL/Tools/datatype_package.ML (2 weeks) Eigene IsaWin-Instanz mit CASL-RS statt HOL-RS HOL-CASL Simplifier: CATS/HOL-CASL/simplifier.sml (1 week) HOL-CASL tactics: CATS/HOL-CALS/tactic.sml (2 days) HOL-CASL encoding: CATS/HOL-CASL/basic_encode.sml (1 day) Encoding of structured free (3 days) Encoding of structured cofree (2 weeks) Eingabesyntax als Mix zwischen CASL und HOL (3 days) Adapt Isabelle unions to CASL unions (1 week) IsaWin git/src/isa_ext/casl_thy.sml (1 week) Generate Proof obligations (1 week) Add renaming to Isabelle kernel (2 months) Basic datatypes CASL-lib/Basic/basic.casl Repository mit korrekten und fehlerhaften Specs CATS User manual, Doku fuer Environments (2 weeks) CASL tool set=>ML page http://www.cs.princeton.edu/~appel/smlnj/projects.html Integration mit Consistency checker Mehr Beweiser anbinden Logic graph display Translation HetCASL -> to development graph Modal logic, equational logic Module graph in Lisp verkapseln /home Printer LaTeX generation: CATS/latex/generator.sml (3 months) GraphDisplay-Tool (uni/appl/dev_graph) Nach linux portieren Schließen der Fenster ohne "Absturz" Wiederherstellen des alten Graphen "Äußere" interne Knoten bei "Hide internal nodes" genau so wie die externen Knoten darstellen (auch die von ihnen ausgehenden Kanten) Dokumentation in Lisp verkapseln /home/cofi/jorina/acl/doc/acldoc-pdfs/aclug.pdf Möglichkeit zum Verstecken von internen Knoten Anzeigen von Menüs