atiti
commented
11 years ago From: (GH: None) Date: Sat Dec 15 17:23:02 2007
added mailto line
This message has 0 attachment(s)
Open atiti opened 11 years ago
atiti
commented
11 years ago From: (GH: None) Date: Sat Dec 15 17:23:02 2007
added mailto line
This message has 0 attachment(s)
atiti
commented
11 years ago From: dcochran (GH: dcochran) Date: Thu Jan 17 16:26:50 2008
Adding related notes from #367:
Add a new switch -javacard
Adding support for such will entail:
o shipping the Java Card API that has been developed in Nijmegen. This jar file of specs replaces the portions of jmlspecs.jar that specify core Java classes (e.g., java.lang). This might mean we have to split jmlspecs.jar into two pieces, based upon some feedback I have received from Erik.
o disable some types. Java Card 2.x supports integral types byte, char, and short but not int or long. Later/alternate versions of Java Card support ints. This variance is why we'll probably need an optional
atiti
commented
11 years ago From: dcochran (GH: dcochran) Date: Thu Jan 17 17:27:20 2008
So, we need a platform switch, with various options: e.g.
-platform java 1.5 or -platform javacard 2.0
... check to see if KindOptions will support this ...
atiti
commented
11 years ago From: dcochran (GH: dcochran) Date: Thu Jan 17 17:28:27 2008
atiti
commented
11 years ago From: dcochran (GH: dcochran) Date: Mon Jun 30 11:36:23 2008
Milestone ESCJava2.0b5 release deleted
{{{
!html
Reply to: noreply@sort.ucd.ie }}} {{{ Research item #195, was opened at 2005-10-26 12:15 You can respond by visiting: http://sort.ucd.ie/tracker/?func=detail&atid=780&aid=195&group_id=97
Category: Architecture Group: None
Initial Comment: Erik Poll and Engelbert Hubbers at Radboud University Nijmegen wrote specifications for the JavaCard 2.x platform. These specs were checked against the JavaCard reference implementation that shipped with JavaCard 2.1.1. (Later versions of the JavaCard 2.x releases from Sun did not include a reference implementation.) The specs were checked originally with SRC ESC/Java, and later with an early release of ESC/Java2.
ESC/Java2 (and later, the Mobius Tool/IVE) should have the capability to reason about alternative versions of Java in a rational manner. Right now we have a -source switch, exactly like javac. When -source 1.4 is specified, we parse and reason about Java 1.4 assert statements. This is a small example of such capability.
At this time, this capability is deeply integrated in the architecture. The purpose of this research project is to think about how to make this capability more abstract and attach parsing, reasoning, and specifications to specific input and output features (e.g., different language variants, different VC generators, different theorem provers).
The initial case studies that can be used for such an architecture are the quartet of variants that we wish to support with the current ESC/Java2 architecture in the near future: Java <1.4, Java 1.4, JavaCard 2.x, and MIDP 1.0. MIDP is the standard that we must support for Mobius work.
Thus, the initial work on this project is adding support for a -source javacard switch. The presence of such a switch would indicate to ESC/Java2 that the JavaCard specs should be used in lieu of the core JDK specs that we currently use. We can ship the JavaCard specs with ESC/Java2 without issue.
Note that this issue is more subtle than just choosing a specific set of specs. JavaCard 2.x, for example, does not support floating point types nor threads. So quality support for such a switch should automatically detect the use of such features and signal a warning to the user. Additionally, because such feature cannot exist in a JavaCard program, the background theory for extended static checking should/need not include the associated axioms and lemmas for reasoning about such constructs.
Initial researchers: Joe Kiniry, Erik Poll
You can respond by visiting: http://sort.ucd.ie/tracker/?func=detail&atid=780&aid=195&group_id=97 }}}