[CZT-Devel] CZT new features (take 1)

[Leo F. <leo...@ne...>]

Hi all,

As promised, prior to the upcoming release we tried to collect the "activity" within CZT 
in the past few years with the major udpates/developments divided by categories of 
functionality, improvement, IDE, and admin. 

The list is not exhaustive and we will add it to the website as "features" and try to keep 
them up-to date as much as possible. Thanks to Andrius efforts on nightly builds and
the website this should be straightforward to do now :-).

Best,
Leo & Andrius

=== New functionality ===

* Z Verification Condition Generator
	= Z VC infrastructure: 	
		+  DefinitionTable extension to infer declared types,
	   		and schema calculus usage within specs
		+ Predicate transformers for VC automatic simplification
		+ file-based and programmable integration

	= Domain Checking VCs for consistency of function application, 
	   definite description (\mu), and unique existential quantification 

	= Feasibility VCs for precondition calculation over a given state and operations
		+ user-defined configuration as a special schema determines what VCs to generate
		+ VCs generated according to a prescribed pattern, including state initialisation
		+ Added signature schemas for modular generation of VCs
		+ Added VCs for axiomatic definitions consistency and given type non-emptyness
		+ File-based VC generation (i.e. result is a new section with VCs)
		+ Eclipse integration to ensure all VCs generated are accounted for in Spec

	= Refinement VCs for forward/backward simulation 
		+ support for interface refinement rules
		+ takes initialisation and finalisation into account
		+ user-defined configuration as a special schema determining VCs to generate
		+ VCs for correctness, applicability, init/final, and I/O

* New language extensions (i.e. AST, parser, printer, type checker, IDE integration)	
	= ZEves proof language integration
	= Circus Jokers / Wildcards for Rules

	(Under development)
	= Circus time
	= Object Oriented Circus (Oh Circus)
	= Oh Circus extended with pointers and Time

* ZEves integration
	= Iso-Z (CZT) to Fuzz-like-Z (ZEves) translator
	= CZT-XML to EVES-XML input 
	= EVES-XML output to CZT (Unicode and LaTeX)
	= interpretation of ZEves results  (i.e. lemmas used, new prover goals, etc)
	= ZEves session useful for extending tools to interact/inspect/interfere with the proof session
	= Socket-based connection to the EVES server (i.e. completely subsumes ZEves front-end interfaces)
	= extended parser/printer to copy with new proof commands and proof environment  
	= session snapshots to enable integration with proof inspection tools for replay / learning from proof attempts (see www.ai4fm.org)
	= programmable encoding of new proof tactics
	= extensive test set from Grand Challenge repository of experiments (i.e. Tokeneer, Mondex, POSIX file stores, Flash Memory, etc).

* experimental
	= z2b translation
	= z2alloy translation
	= ZEves jEdit plugin

=== Improvements ===

* improved memory management of names
	= memory profiling to detected/fixed leaks in parser I/O, Factory classes, and AST default list sizes (now zeroed) (55% memory footprint decrease)
	= traceability of AST instances for aiding debugging of dangling references and future memory leaks
	= traceability of ZName usage/creation as it became the key AST class for memory improvement/usage

	= TODO: recent discovery of Signature copying in type checker leading to possible memory improvement (under investigation) 

* section management
	= transaction-based section management for improved performance on large specifications (i.e. avoid reparsing/typechecking)
		+ avoids reloading of sections
		+ takes transitive dependencies into account (up/downwards and diamond dependencies)
		+ widened scope of transaction in case of low-level parsers like LaTeXMarkupScanner, which bootstraps high-level parsing

	= normalised access to standard/known Sections 
	= normalised access to SectionManager through explicit use of extension/dialect of interest
	= SectionManager performance and documentation improvements  

* code warnings and generics
	= CZT had about 10000 warnings across various projects, now it has 6!
  		(this was partially historic --- Java Generics ---, 
		 partly dependant on external tools --- CUP/GnAST code generated with warnings,
		 partially coding practices to avoid now easily captured by IDEs). 
		Overall the exercise normalised code, improved clarity and rooted
		out some tricky real bugs from these warnings.

	= remainder warnings are now to be taken as features being or yet to being implemented. 

* low-level tools update: GnAST
	= GNAsT update as a maven plugin with extra controlling parameters
	= Corejava build per extension to avoid slow rebuilds
	= warning-free code generation + generics aware code
	= added debugging information for Velocity generation
	= proper handling of Enum types from ZML declarations
	= fixed bugs on list handling and JAXB property elements for XML integration

* low-level tools update: java-CUP
	= can cope with large grammars as external files (i.e. Circus onwards generated Java file beyond allowed size).
	= better debugging information for grammar-code generation to allow for fine-tuning and warning elimination

* low-level tools update: others
	= update use of logging to be more consistent across various tools
	= added warning manager across developments
	= basic CZTManagedTestCase class for consistent test case coding standard

=== IDE ===

* Extended Eclipse integration
	= CZT-ide product as a standalone Eclipse application
	= basic for Circus and Object-Z (i.e. use of type checker + extended char map)
	= thorough for Z and ZEves (i.e. syntax highlight, auto-completion, various squiggles, outline, etc).
	= VCG integration with theorems proved / to-prove view
	= ZEves link/integration via Z-XML Api
	= various markup conversions and type checking information as tooltips

* Website update
	= modern look-and-feel
	= markdown-based website for easy extension
	= wiki-like document ion based on text files

=== Adeministrative ===

* Move to Git
	= easy of branch/merge for parallel (independent) developments
	= fine-grained control of commits and histories

* Improved documentation
	= added java doc at key (mostly requested) parts (i.e. section manager, parsing, lang-extension etc)
	= installation, update, build documentation and instructions (including for Eclipse builds)

* Project separation / rearrangement
	= parent maven project for: vcg, corejava, type checker, parser, etc
	= this enables uniform maven integration and dependency checking
	= also helps IDE integration for development with Eclipse and Netbeans
	= easier for new language extensions

* Nightly builds via Jenkins server
	= automatic nightly builds of czt.jar, IDEs (jEdit + Eclipse)
	= automatic javadoc and website builds