Posts by author frankrimlinger@NEXT.ARC.NASA.GOV

Mango plugin for Eclipse Workbench is ready

As advertised at the Workshop, the Mango plugin for the Eclipse workbench is ready for use. For examples and installation instructions, see jpf-mango.

Mango builds a functional model of Java code, exposed as navigable browser pages. When used as a sanity checker, Mango will halt at every case-split, allowing the programmer to compare source code with generated model.

As an educational tool. Those learning Java as a first programming language have the opportunity to compare procedural and functional views of code. This comparison facilitates the exposition of formal modeling concepts. For this purpose, the Mango installation contains a comprehensive set of first year Java code examples, such as CarRecall

Mango may potentially be used to generate and apply filters for known Java security issues, see for example Oracle guidelines Currently this is the active area of development. Waiting in the wings is formal theorem proving, see these comments.

Added page for hosting Eclipse plugin

I have added a page describing Sandro's method for hosting an Eclipse plugin. You have to do it from the wiki, I am convinced now you cannot do it (or at least should not do it) from the repository. See hosting an Eclipse plugin update site.

Eclipse workbench port of jpf-mango underway

Happily, jpf-mango has matured fast enough to justify a port to the Eclipse workbench. For details, see

jpf-mango First Example

The jpf-mango project has produced its first? totally automated, not-completely-trivial specification of sample java code. The project code base contains standard and exotic embeddings of the jpf engine.