JSizzle (Java Specifications In Z Language Extension) is a derivation of the Java language which enables the specification of software behaviour at an abstract level.
The goal of JSizzle is to create a simple, achievable incursion of formal methods into new areas of mainstream software engineering by leaning heavily on familiarity of syntax and tools.
JSizzle is a cross-platform utility capable of running on any operating system that comes with Java support (e.g. Mac OS X, Windows, Linux).
Here are some key features of "JSizzle":
· Are easy for Java programmers to create and understand
· Make use of existing Java tools such as development environments
· Can be used to instrument executable code with assertion checking
· Make minimal use of Java annotations
· Are based on the Z notation, and could be converted to (and from) Z for formal analysis