search

kiniry / Mobius

4 stars 8 forks source link

[ escjava-Feature Requests-248 ] XML or s-expression-based pretty printing #202

Open atiti opened 11 years ago

atiti commented 11 years ago

{{{

!html

Reply to: noreply@sort.ucd.ie }}} {{{ Feature Requests item #248, was opened at 2006-02-23 15:06 You can respond by visiting: http://sort.ucd.ie/tracker/?func=detail&atid=444&aid=248&group_id=97

Category: Interface Improvements Group: None

Status: Closed Resolution: Out of Date Priority: 1 Submitted By: Joseph Kiniry (jkiniry) Assigned to: Nobody (None) Summary: XML or s-expression-based pretty printing

Initial Comment: A recent discussion on JMLSpecs-interest got me thinking about this topic.

Having a general purpose XML-based or s-expression-centric pretty-printing facility is of general use for tools like ESC/Java2 and the JML tool suite. These generic representation formats have also come up in the context of the Proof General Toolkit, PVS, and the Mobius tool.

Here is the exchange that provides sufficient context for this feature request:

Hi JML folks,

Is there an easy way to take a JML-annotated Java source file and print out its abstract syntax tree (ideally, with parentheses to indicate the tree structure)?

I'm using the theorem prover ACL2 to verify Java bytecode programs, and I'd like to make use of JML annotations. To do that I need, at the very least, an easy way to parse JML.

Thanks! -Eric Smith, Stanford University

Hi Eric,

There is a disused option of the ISU JML tools, those available through the jmlspecs and multijava sourceforge projects, which was intended to output XML format for the parsed programs. I think that perhaps could be fairly easily updated (to work) and then adapted to your needs.

Gary

Hi all,

Just to mention that if such a XML output exist, in the Krakatoa project we would be interested to use it too. We indeed made an attempt to build such an XML output from the multijava sources, and we met difficulties, which required a significant modification of the code so we gave up. Some of the requirements we had :

1) The XML output must keep track in some way how the scope of identifiers has been resolved: the variable identifiers for example, occuring either in the Java code or in the specs, must be linked to their declaration, via a unique integer id for example. Other example is the resolution of the overloading: each method call must be linked to the corresponding method declaration.

2) The XML output must not only represent the source code, but also all the environment of it, that is all the API classes used. In other words, the XML must be self-contained.

3) We would also need to get the XML output after the desugaring phase.

Any chance this could be possible ?

You can respond by visiting: http://sort.ucd.ie/tracker/?func=detail&atid=444&aid=248&group_id=97 }}}

atiti commented 11 years ago

From: (GH: None) Date: Sat Dec 15 17:21:51 2007

added mailto line

This message has 0 attachment(s)

atiti commented 11 years ago

From: None (GH: None) Date: Tue Apr 27 14:34:16 2010

Milestone ESCJava2 2.0.9 release deleted

atiti commented 11 years ago

From: kiniry (GH: kiniry) Date: Fri Apr 30 14:27:58 2010

There seemed to be interest in this, but it is probably superseded by the new JIR libraries.