jmlRewrite

details see accompanying e-mail

eclipse/.project

@@ -18,14 +18,14 @@
 	</natures>
 	<linkedResources>
 		<link>
-			<name>tcc_modules</name>
+			<name>key_lib</name>
 			<type>2</type>
-			<locationURI>tcc_modules</locationURI>
+			<locationURI>key_lib</locationURI>
 		</link>
 		<link>
-			<name>key_lib</name>
+			<name>tcc_modules</name>
 			<type>2</type>
-			<locationURI>key_lib</locationURI>
+			<locationURI>tcc_modules</locationURI>
 		</link>
 	</linkedResources>
 </projectDescription>

examples/_testcase/speclang/testFile.key

@@ -0,0 +1,3 @@
+\javaSource "testPackage";
+
+\problem { true }

examples/_testcase/speclang/testPackage/TestClass.java

@@ -0,0 +1,25 @@
+package testPackage;
+
+public class TestClass {
+
+    int i;
+    long l;
+
+    public int getOne() {
+        return 1;
+    }
+
+    public int m(int a) {
+        return 2;
+    }
+
+    public int m(long a) {
+        return 3;
+    }
+
+    public static int staticMethod() {
+        return 4;
+    }
+
+}
+

examples/java_dl/for_demo/For.java

@@ -0,0 +1,117 @@
+class For {
+
+    /* This method should be proven automatically since the contract
+     * of the for loop is transferred to the generated while loop
+     */
+
+    /*@ requires length > 0;
+      @ ensures \result == length;
+      @*/
+    public int annotations(int length) {
+	int count = 0;
+
+	/*@ loop_invariant i >= 0 & i <= length & count == i;
+	  @ decreasing length - i;
+          @ assignable count, i;
+	  @*/
+	for(int i = 0; i < length; i++) {
+	    count = count + 1;
+	}
+
+	return count;
+    }
+
+
+    /* 
+     * This method should be proven automatically since the contract
+     * of the for loop is transferred to the generated while loop
+     */
+
+    /*@ requires array != null && array.length > 0;
+      @ ensures (\forall int i; i >= 0 && i < \old(array).length; \result <= \old(array)[i]);
+      @ ensures (\forall int i; i >= 0 && i < \old(array).length; array[i] == \old(array)[i]);
+    */
+    public int array_min(int[] array) {
+
+	int min = array[0];
+
+	/*@ loop_invariant (\forall int j; j >= 0 && j < i; min <= array[j]);
+	  @ assignable i, min;
+	  @ decreasing array.length - i;
+	*/
+	for(int i = 1; i < array.length; i++) {
+	    if(min > array[i])
+		min = array[i];
+	}
+
+	return min;
+    }
+
+
+    /*
+     * This method is used to show that loops are treated correctly
+     * even if parts are left out.
+     */
+
+    /*@ requires true;
+      @ ensures true;
+    */
+    public void leave_out() {
+
+	for(int i = 0; i < 100;) { break; }
+	for(int i = 0; ;i++) { break; }
+	for(;;) { break; }
+
+    }
+
+
+    /*
+     * This method checks whether breaks and continues are handled
+     * correctly.
+     */
+
+    /*@ requires true;
+      @ ensures \result;
+    */
+    public boolean checkBreakContinue() {
+	int dummy;
+	boolean ret = true;
+
+	outerlabel: {
+	    dummy = 0;  // some statement
+	    for(;dummy == 0;dummy++) {
+		break outerlabel;
+	    }
+	}
+
+	// dummy must be 0 here
+	ret &= (dummy == 0);
+
+	dummy = 0;
+	for(; dummy == 0; dummy++) {
+	    break;
+	}
+	// dummy must be 0 here
+	ret &= (dummy == 0);
+
+	dummy = 0;
+	for(; dummy == 0; dummy++) {
+	    continue;
+	}
+	// dummy must be 1 here
+	ret &= (dummy == 1);
+
+	dummy = 0;
+	outer: while(dummy == 0) {
+	    dummy = 1;
+	    for(; true; dummy++) {
+		continue outer;
+	    }
+	}
+	// dummy must be 1 here
+	ret &= (dummy == 1);
+
+	return ret;
+
+    }
+}

examples/java_dl/payCardOCL/paycard/CardException.java

@@ -0,0 +1,5 @@
+public class CardException extends java.lang.Exception{
+
+    public CardException(){
+    }
+}

examples/java_dl/payCardOCL/paycard/ChargeUI.java

@@ -0,0 +1,95 @@
+/* Generated by Together */
+
+import javax.swing.*;
+import java.awt.event.ActionEvent;
+import java.awt.event.ActionListener;
+import java.awt.*;
+
+public class ChargeUI {
+
+	ChargeUI(int desiredCardType, int limit){
+        frame = new JFrame("Charge Paycard");
+        jTextArea1.setFont(new Font("",Font.PLAIN, 18));
+	if (desiredCardType==IssueCardUI.STANDARD){
+            this.limit=1000;
+	    paycard = new PayCard();
+        } else if (desiredCardType==IssueCardUI.JUNIOR){
+	    this.limit=100;
+            paycard = PayCardJunior.createCard();
+        } else if (desiredCardType==IssueCardUI.USER_DEFINED){
+            this.limit=limit;
+            paycard = new PayCard(limit);
+        }
+    }
+
+    public void initGUI() {
+      	jButton2.setText("Quit");
+      	jButton2.addActionListener(new ActionListener(){public void actionPerformed(ActionEvent e){jButton2ActionPerformed(e);}});
+      	jButton1.setText("charge");
+      	jButton1.addActionListener(new ActionListener(){public void actionPerformed(ActionEvent e){jButton1ActionPerformed(e);}});
+      	frame.setBounds(100,100,550,350);
+        frame.setResizable(true);
+        frame.setDefaultCloseOperation(javax.swing.JFrame.EXIT_ON_CLOSE);
+        jTextField1.setText("jTextField1");
+        frame.getContentPane().setLayout(new BorderLayout());
+        frame.getContentPane().add(new JPanel(),BorderLayout.WEST);
+        frame.getContentPane().add(new JPanel(),BorderLayout.EAST);
+        frame.getContentPane().add(jPanel1,BorderLayout.CENTER);
+        frame.getContentPane().add(jPanel2,BorderLayout.SOUTH);
+        jPanel2.setLayout(new GridLayout(1,2));
+        jPanel2.add(jButton1);
+        jPanel2.add(jButton2);
+        jPanel1.setLayout(new BorderLayout());
+        jPanel3.setLayout(new GridLayout(1,2));
+        jPanel3.add(jLabel1);
+        jPanel3.add(jTextField1);
+        jPanel1.add(jPanel3,BorderLayout.SOUTH);
+        jPanel1.add(jTextArea1);
+        jPanel1.add(jLabel2,BorderLayout.NORTH);
+        jLabel1.setText("Amount to charge:");
+        jTextField1.setText("");
+        jTextArea1.setText("");
+        jTextArea1.setBorder(javax.swing.BorderFactory.createEtchedBorder());
+        jTextArea1.setEditable(false);
+        JScrollPane jScrollPane1 = new JScrollPane(jTextArea1);
+        jScrollPane1.setHorizontalScrollBarPolicy(javax.swing.JScrollPane.HORIZONTAL_SCROLLBAR_AS_NEEDED);
+        jPanel1.add(jScrollPane1, null);
+        jLabel2.setText("Limit of paycard is "+limit+".");
+        jLabel2.setFont(new java.awt.Font("SansSerif", java.awt.Font.BOLD, 14));
+        frame.show();
+    }
+
+    public void jButton2ActionPerformed(ActionEvent e) {
+        frame.dispose();
+        System.exit(0);
+    }
+
+    public void jButton1ActionPerformed(ActionEvent e) {
+        // read textfield
+        int charge;
+        try{
+            charge=Integer.parseInt(jTextField1.getText());
+        }
+        catch (NumberFormatException ex){
+           JOptionPane.showMessageDialog(
+                frame, "Amount to charge has to be a number!", "Error",
+                JOptionPane.ERROR_MESSAGE);
+            return;
+        }
+		paycard.charge(charge);
+        jTextArea1.append(paycard.infoCardMsg()+"\n");
+    }
+
+    private JFrame frame;
+    private int limit;
+    private JPanel jPanel1 = new JPanel();
+    private JPanel jPanel2 = new JPanel();
+    private JPanel jPanel3 = new JPanel();
+    private JLabel jLabel1 = new JLabel();
+    private JTextField jTextField1 = new JTextField();
+    private JButton jButton2 = new JButton();
+    private PayCard paycard;
+    private JButton jButton1 = new JButton();
+    private JTextArea jTextArea1 = new JTextArea();
+    private JLabel jLabel2 = new JLabel();
+}

examples/java_dl/payCardOCL/paycard/IssueCardUI.java

@@ -0,0 +1,127 @@
+import javax.swing.JPanel;
+import javax.swing.JRadioButtonMenuItem;
+
+import javax.swing.*;
+import java.awt.*;
+import java.awt.event.ActionEvent;
+import java.awt.event.ActionListener;
+
+public class IssueCardUI{
+
+    public IssueCardUI(){
+        frame = new JFrame("Issue Paycard");
+        desiredCardType=STANDARD;
+    }
+
+    public void initGUI() {
+	frame.setBounds(100,100,550,230);
+        frame.setResizable(true);
+        frame.setDefaultCloseOperation(javax.swing.JFrame.EXIT_ON_CLOSE);
+        frame.getContentPane().setLayout(new BorderLayout());
+        frame.getContentPane().add(new JPanel(),BorderLayout.WEST);
+        frame.getContentPane().add(new JPanel(),BorderLayout.EAST);
+        frame.getContentPane().add(jPanel1,BorderLayout.CENTER);
+	frame.getContentPane().add(jPanel2,BorderLayout.SOUTH);
+        GridLayout layout = new GridLayout(3,1);
+        jPanel1.setLayout(layout);
+        jPanel2.setLayout(new GridLayout(1,3));
+        jPanel3.setLayout(new GridLayout(1,3));
+        jPanel5.setLayout(new BorderLayout());
+        jPanel1.add(jRadioButton1);
+        jPanel1.add(jRadioButton2);
+       	jPanel1.add(jPanel3,BorderLayout.SOUTH);
+        jPanel3.add(jRadioButton3);
+        jPanel2.add(jButton1);
+        jPanel2.add(jButton2);
+        jPanel4.setLayout(new BorderLayout());
+        jPanel4.add(jLabel1,BorderLayout.EAST);
+        jPanel3.add(jPanel4);
+        jPanel5.add(new JPanel(),BorderLayout.NORTH);
+        jPanel5.add(new JPanel(),BorderLayout.SOUTH);
+        jPanel5.add(jTextField1,BorderLayout.CENTER);
+        jPanel3.add(jPanel5);
+        jRadioButton1.setText("jRadioButton1");
+        jRadioButton1.setLabel("Standard Paycard");
+        jRadioButton1.setSelected(true);
+        jRadioButton2.setText("jRadioButton2");
+        jRadioButton2.setLabel("Junior Paycard");
+        jRadioButton3.setText("jRadioButton3");
+        jRadioButton3.setLabel("User Defined Paycard");
+        jButton1.setText("jButton1");
+        jButton1.setLabel("Issue Paycard");
+        jButton2.setText("jButton2");
+        jButton2.setLabel("Quit");
+        jTextField1.setText("1000");
+        jTextField1.setMaximumSize(new Dimension(200,10));
+        jTextField1.setMinimumSize(new Dimension(200,10));
+        jTextField1.setPreferredSize(new Dimension(200,10));
+        jLabel1.setText("Limit:  ");
+        jLabel1.setToolTipText("Limit of the paycard");
+        ButtonGroup group = new ButtonGroup();
+        group.add(jRadioButton1);
+        group.add(jRadioButton2);
+        group.add(jRadioButton3);
+        RadioListener listener = new RadioListener();
+        jRadioButton1.addActionListener(listener);
+	jRadioButton2.addActionListener(listener);
+	jRadioButton3.addActionListener(listener);
+        frame.show();
+        jButton2.addActionListener(new ActionListener(){public void actionPerformed(ActionEvent e){jButton2ActionPerformed(e);}});
+        jButton1.addActionListener(new ActionListener(){public void actionPerformed(ActionEvent e){jButton1ActionPerformed(e);}});
+    }
+
+    public void jButton2ActionPerformed(ActionEvent e) {
+        frame.dispose();
+        System.exit(0);
+    }
+
+    public void jButton1ActionPerformed(ActionEvent e) {
+        // read textfield
+        int limit=0;
+        if (desiredCardType==USER_DEFINED){
+            try{
+            	limit=Integer.parseInt(jTextField1.getText());
+            }
+            catch (NumberFormatException ex){
+            	JOptionPane.showMessageDialog(
+                	frame, "Limit has to be a number!", "Error",
+                	JOptionPane.ERROR_MESSAGE);
+                return;
+            }
+        }
+        frame.dispose();
+	ChargeUI chargeUI = new ChargeUI(desiredCardType, limit);
+        chargeUI.initGUI();
+    }
+
+    class RadioListener implements ActionListener{
+	public void actionPerformed(ActionEvent e){
+            if (e.getActionCommand().equals("Standard Paycard")){
+                desiredCardType=STANDARD;
+            } else if (e.getActionCommand().equals("Junior Paycard")){
+                 desiredCardType=JUNIOR;
+            } else if (e.getActionCommand().equals("User Defined Paycard")){
+                 desiredCardType=USER_DEFINED;
+            }
+        }
+    }
+
+
+    private JFrame frame;
+    private JPanel jPanel1 = new JPanel();
+    private JPanel jPanel2 = new JPanel();
+    private JPanel jPanel3 = new JPanel();
+    private JPanel jPanel4 = new JPanel();
+    private JPanel jPanel5 = new JPanel();
+    private JRadioButton jRadioButton1 = new JRadioButton();
+    private JRadioButton jRadioButton2 = new JRadioButton();
+    private JRadioButton jRadioButton3 = new JRadioButton();
+    private JButton jButton1 = new JButton();
+    private JButton jButton2 = new JButton();
+    private JTextField jTextField1 = new JTextField();
+    private JLabel jLabel1 = new JLabel();
+    protected final static int STANDARD=1;
+    protected final static int JUNIOR=2;
+    protected final static int USER_DEFINED=3;
+    private int desiredCardType;
+}