Node.java Source File

00001 package edu.ksu.cis.bandera.abstraction.pvs;
00002 
00003 /* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
00004  * Bandera, a Java(TM) analysis and transformation toolkit           *
00005  * Copyright (C) 1999, 2000   Corina Pasareanu (pcorina@cis.ksu.edu) *
00006  * All rights reserved.                                              *
00007  *                                                                   *
00008  * This work was done as a project in the SAnToS Laboratory,         *
00009  * Department of Computing and Information Sciences, Kansas State    *
00010  * University, USA (http://www.cis.ksu.edu/santos).                  *
00011  * It is understood that any modification not identified as such is  *
00012  * not covered by the preceding statement.                           *
00013  *                                                                   *
00014  * This work is free software; you can redistribute it and/or        *
00015  * modify it under the terms of the GNU Library General Public       *
00016  * License as published by the Free Software Foundation; either      *
00017  * version 2 of the License, or (at your option) any later version.  *
00018  *                                                                   *
00019  * This work is distributed in the hope that it will be useful,      *
00020  * but WITHOUT ANY WARRANTY; without even the implied warranty of    *
00021  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU *
00022  * Library General Public License for more details.                  *
00023  *                                                                   *
00024  * You should have received a copy of the GNU Library General Public *
00025  * License along with this toolkit; if not, write to the             *
00026  * Free Software Foundation, Inc., 59 Temple Place - Suite 330,      *
00027  * Boston, MA  02111-1307, USA.                                      *
00028  *                                                                   *
00029  * Java is a trademark of Sun Microsystems, Inc.                     *
00030  *                                                                   *
00031  * To submit a bug report, send a comment, or get the latest news on *
00032  * this project and other SAnToS projects, please visit the web-site *
00033  *                http://www.cis.ksu.edu/santos                      *
00034  * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
00035 import java.io.*;
00036 
00037 public class Node {
00038  int token;
00039  Integer value;
00040  String id_value;
00041  Node left=null;
00042  Node right=null;
00043 
00044  static int n=0;
00045 
00046  public Node(int t, Node n) {
00047     token=t;
00048         left=n;
00049  } 
00050  public Node(int t, Node l,Node r) {
00051     token=t;
00052     left=l;
00053         right=r;
00054  } 
00055  public Node(int t, Integer v) {
00056     token=t;
00057     value=v;
00058  } 
00059  public Node(int t, String s) {
00060     token=t;
00061         id_value=s;
00062  } 
00063  public Node(int t, String s, Node n) {
00064     token=t;
00065         left=n;
00066         id_value=s;
00067  } 
00068  /* print AST for generated BASL spec */
00069  public void print_BASL(PrintWriter f_spec) {
00070 
00071        switch (token)
00072        {
00073         case sym.SEMI: if (right==null) {
00074                  f_spec.print("    ");
00075                          left.print_BASL(f_spec);
00076                          f_spec.print(" -> " + id_value + " ;\n");
00077                        } else {
00078                                 left.print_BASL(f_spec);
00079                                 right.print_BASL(f_spec);
00080                               }
00081                        break;
00082         case sym.OR: left.print_BASL(f_spec);f_spec.print("||");
00083             right.print_BASL(f_spec);break;
00084         case sym.AND:left.print_BASL(f_spec);f_spec.print("&&");
00085             right.print_BASL(f_spec);break;
00086         case sym.EQ: left.print_BASL(f_spec);f_spec.print("==");
00087             right.print_BASL(f_spec);break;
00088         case sym.NE: left.print_BASL(f_spec);f_spec.print("!=");
00089             right.print_BASL(f_spec);break;
00090         case sym.LE: left.print_BASL(f_spec);f_spec.print("<=");
00091             right.print_BASL(f_spec);break;
00092         case sym.LT: left.print_BASL(f_spec);f_spec.print("<");
00093             right.print_BASL(f_spec);break;
00094         case sym.GE: left.print_BASL(f_spec);f_spec.print(">=");
00095             right.print_BASL(f_spec);break;
00096         case sym.GT: left.print_BASL(f_spec);f_spec.print(">");
00097             right.print_BASL(f_spec);break;
00098         case sym.PLUS:left.print_BASL(f_spec);f_spec.print("+");
00099             right.print_BASL(f_spec);break;
00100         case sym.MINUS:left.print_BASL(f_spec);f_spec.print("-");
00101             right.print_BASL(f_spec);break;
00102         case sym.TIMES:left.print_BASL(f_spec);f_spec.print("*");
00103             right.print_BASL(f_spec);break;
00104         case sym.DIV:left.print_BASL(f_spec);f_spec.print("/");
00105             right.print_BASL(f_spec);break;
00106         case sym.MOD:left.print_BASL(f_spec);f_spec.print("%");
00107             right.print_BASL(f_spec);break;
00108         case sym.NUMBER: f_spec.print(" "+value+" ");break;
00109         case sym.ID: f_spec.print(" "+id_value+" ");break;
00110         case sym.UMINUS: f_spec.print("-");left.print_BASL(f_spec);break;
00111         case sym.NOT: f_spec.print("!");left.print_BASL(f_spec);break;
00112         case sym.LPAREN:f_spec.print("(");left.print_BASL(f_spec);
00113                         f_spec.print(")");break;
00114         default: break;
00115        }
00116         return;
00117  } 
00118  /* print AST for pvs theory */
00119  public void print_PVS(PrintWriter f_pvs) {
00120 
00121        switch (token)
00122        {
00123         case sym.SEMI: if (right==null) {
00124                          f_pvs.print("P"+n+"(e): boolean = (");n++;
00125                          left.print_PVS(f_pvs);
00126                          f_pvs.println(")");
00127                        } else {
00128                                 left.print_PVS(f_pvs);
00129                                 right.print_PVS(f_pvs);
00130                               }
00131                        break;
00132         case sym.OR: left.print_PVS(f_pvs);f_pvs.print("OR");
00133             right.print_PVS(f_pvs);break;
00134         case sym.AND:left.print_PVS(f_pvs);f_pvs.print("AND");
00135             right.print_PVS(f_pvs);break;
00136         case sym.EQ: left.print_PVS(f_pvs);f_pvs.print("=");
00137             right.print_PVS(f_pvs);break; 
00138         case sym.NE: left.print_PVS(f_pvs);f_pvs.print("/=");
00139             right.print_PVS(f_pvs);break;
00140         case sym.LE: left.print_PVS(f_pvs);f_pvs.print("<=");
00141             right.print_PVS(f_pvs);break;
00142         case sym.LT: left.print_PVS(f_pvs);f_pvs.print("<");
00143             right.print_PVS(f_pvs);break;
00144         case sym.GE: left.print_PVS(f_pvs);f_pvs.print(">=");
00145             right.print_PVS(f_pvs);break;
00146         case sym.GT: left.print_PVS(f_pvs);f_pvs.print(">");
00147             right.print_PVS(f_pvs);break;
00148         case sym.PLUS:left.print_PVS(f_pvs);f_pvs.print("+");
00149             right.print_PVS(f_pvs);break;
00150         case sym.MINUS:left.print_PVS(f_pvs);f_pvs.print("-");
00151             right.print_PVS(f_pvs);break;
00152         case sym.TIMES:left.print_PVS(f_pvs);f_pvs.print("*");
00153             right.print_PVS(f_pvs);break;
00154         case sym.DIV:left.print_PVS(f_pvs);f_pvs.print("/");
00155             right.print_PVS(f_pvs);break;
00156         case sym.MOD:left.print_PVS(f_pvs);f_pvs.print("//");
00157             right.print_PVS(f_pvs);break;
00158         case sym.NUMBER: f_pvs.print(" "+value+" ");break;
00159         case sym.ID: f_pvs.print(" e ");break;
00160         case sym.UMINUS: f_pvs.print("-");left.print_PVS(f_pvs);break;
00161         case sym.NOT: f_pvs.print("NOT");left.print_PVS(f_pvs);break;
00162         case sym.LPAREN:f_pvs.print("(");left.print_PVS(f_pvs);
00163                         f_pvs.print(")");break;
00164         default: break; 
00165        }
00166         return;
00167  } 
00168 }