Main Page   Packages   Class Hierarchy   Alphabetical List   Compound List   File List   Compound Members  

PVS.java

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 import java.util.*;
00037 
00038 public class PVS {
00039   public static Vector proofs; /* contains pvs proofs */
00040 
00041 /* builds the antet of a pvs theory for float */
00042  public static void begin_float(PrintWriter f_pvs) {
00043     f_pvs.print("abstraction: THEORY\n\nBEGIN\n\n");
00044         f_pvs.print(" b: VAR boolean\n");
00045         f_pvs.print(" TRUE?(b): boolean = (b=TRUE)\n");
00046         f_pvs.print(" FALSE?(b): boolean = (b=FALSE)\n\n");
00047         f_pvs.print(" \n");
00048         f_pvs.print(" e,e1,e2: VAR real\n");
00049         f_pvs.print(" nz_e: VAR {e | e/=0}\n");
00050  } 
00051 /* builds the antet of a pvs theory for int */
00052  public static void begin_int(PrintWriter f_pvs) {
00053         f_pvs.print("basic1: THEORY\n\nBEGIN\n\n");
00054         f_pvs.print(" e1: VAR int\n e2: VAR {e:int|e/=0}\n");
00055         f_pvs.print(" /(e1,e2) : int = floor(e1/e2)\n END basic1\n\n");
00056         f_pvs.print("basic2: THEORY\n\nBEGIN\n\n");
00057         f_pvs.print(" e1: VAR int\n e2: VAR {e:int|e/=0}\n");
00058         f_pvs.print(" //(e1,e2) : int = e1 - e2*floor(e1/e2)\n");
00059         f_pvs.print(" END basic2\n\n");
00060         
00061         f_pvs.print(" abstraction: THEORY\n\nBEGIN\n\n");
00062         f_pvs.print("IMPORTING basic1\n");
00063         f_pvs.print("IMPORTING basic2\n");
00064         f_pvs.print(" b: VAR boolean\n");
00065         f_pvs.print(" TRUE?(b): boolean = (b=TRUE)\n");
00066         f_pvs.print(" FALSE?(b): boolean = (b=FALSE)\n\n");
00067         f_pvs.print(" \n");
00068         f_pvs.print(" e,e1,e2: VAR int\n");
00069         f_pvs.print(" nz_e: VAR {e | e/=0}\n");
00070 
00071  } 
00072 /* builds the checking for function and default value of pvs theory */
00073  public static void check(PrintWriter f_pvs, int npredicates) {
00074     int i,j;
00075     for(i=0;i<npredicates;i++)
00076       f_pvs.print(" default"+i+": THEOREM P"+i+"(0)\n");
00077 
00078     f_pvs.print(" domain: THEOREM ");
00079     for(i=0;i<npredicates-1;i++)
00080           f_pvs.print(" P"+i+"(e) OR ");
00081     f_pvs.print(" P"+i+"(e)\n");
00082 
00083     f_pvs.print(" overlap: THEOREM ");
00084     for(i=0;i<npredicates;i++)
00085       for(j=i+1;j<npredicates;j++)
00086         f_pvs.print(" NOT(P"+i+"(e) AND P"+j+"(e)) AND ");
00087         f_pvs.print(" TRUE\n\n");   
00088  } 
00089  /* writes the results of check part in abstraction f_spec file */
00090  public static void check_BASL(PrintWriter f_spec, int npredicates,
00091                 Vector tokens) {
00092     int lookahead;
00093 
00094     for(int i=0;i<npredicates;i++) {
00095         lookahead=((Integer)proofs.elementAt(i)).intValue();
00096         if(lookahead==1) { /* PROVED */
00097             f_spec.print("\n  DEFAULT = "+tokens.elementAt(i)+";\n");
00098             i=npredicates;
00099         }
00100     }
00101     lookahead=((Integer)proofs.elementAt(npredicates)).intValue();
00102     if(lookahead==0)  /* UNPROVED */
00103         f_spec.print("/* Warning: abstraction does not cover the concrete domain!!! */\n");
00104     lookahead=((Integer)proofs.elementAt(npredicates+1)).intValue();
00105         if(lookahead==0)  /* UNPROVED */
00106                 f_spec.print("/* Warning: overlapping !!! */\n");
00107     
00108     
00109  } 
00110 /* invokes PVS */
00111  public static void execAndWait(String command) {
00112 
00113     try {
00114         System.out.println(command);
00115         Runtime runtime = Runtime.getRuntime();
00116         Process p = runtime.exec(command);
00117         InputStream commandErr = p.getErrorStream();
00118             InputStream commandOut = p.getInputStream();
00119 
00120             byte [] buffer = new byte[4000];
00121         int count = 0;       // total chars read
00122             int charsAvail = commandErr.available();
00123             if (charsAvail > 0) 
00124                 count = commandErr.read(buffer,count,charsAvail);
00125         
00126         proofs = read(commandOut);
00127 
00128         String output = new String(buffer,0,count);
00129             System.err.println(output);
00130             p.waitFor();
00131             return;
00132         }
00133         catch (Exception e) {
00134             throw new RuntimeException("exec of command '" + command
00135                                        + "' was aborted: \n" + e);
00136         }
00137 
00138  } 
00139 /* builds the prf file */
00140  public static void prf(PrintWriter f_prf, int npredicates, int basic_type)
00141  {
00142   int n; /* theorem number */
00143   int i,j,k;
00144 
00145   /* for each operation generate all the possible combinations 
00146      given by npredicates */
00147 
00148   f_prf.print("(|abstraction|\n");
00149 
00150   for(i=0;i<npredicates;i++)
00151     f_prf.print(" (|default"+i+"| \"\" (GRIND) (SKIP) (SKIP))\n");
00152   f_prf.print(" (|domain| \"\" (GRIND) (SKIP) (SKIP))\n");
00153   f_prf.print(" (|overlap| \"\" (GRIND) (SKIP) (SKIP))\n");
00154 
00155   n=1;
00156   for(i=0;i<npredicates;i++)
00157     for(j=0;j<npredicates;j++)
00158       for(k=0;k<npredicates;k++) {
00159         f_prf.print(" (|add"+n+"| \"\" (GRIND) (SKIP) (SKIP))\n");
00160         n++;
00161       } 
00162 
00163   n=1;
00164   for(i=0;i<npredicates;i++)
00165     for(j=0;j<npredicates;j++)
00166       for(k=0;k<npredicates;k++) {
00167         f_prf.print(" (|sub"+n+"| \"\" (GRIND) (SKIP) (SKIP))\n");
00168         n++;
00169       }
00170 
00171   n=1;
00172   for(i=0;i<npredicates;i++)
00173     for(j=0;j<npredicates;j++)
00174       for(k=0;k<npredicates;k++) {
00175         f_prf.print(" (|mul"+n+"| \"\" (GRIND :THEORIES (\"real_props\")) (SKIP) (SKIP))\n");
00176         n++;
00177       }
00178 
00179   n=1;
00180   for(i=0;i<npredicates;i++)
00181     for(j=0;j<npredicates;j++)
00182       for(k=0;k<npredicates;k++) {
00183         f_prf.print(" (|div"+n+"| \"\" (GRIND :THEORIES (\"real_props\")) (SKIP) (SKIP))\n");
00184         n++;
00185       }
00186 
00187   if(basic_type==sym.INT) {
00188   n=1;
00189   for(i=0;i<npredicates;i++)
00190     for(j=0;j<npredicates;j++)
00191       for(k=0;k<npredicates;k++) {
00192         f_prf.print(" (|rem"+n+"| \"\" (GRIND) (SKIP) (SKIP))\n");
00193         n++;
00194       }
00195   }
00196 
00197   n=1;
00198   for(i=0;i<npredicates;i++)
00199     for(j=0;j<npredicates;j++) {
00200         f_prf.print(" (|eq"+n+"| \"\" (GRIND) (SKIP) (SKIP))\n");
00201         n++;
00202         f_prf.print(" (|eq"+n+"| \"\" (GRIND) (SKIP) (SKIP))\n");
00203         n++;
00204       }
00205 
00206 
00207 
00208   n=1;
00209   for(i=0;i<npredicates;i++)
00210     for(j=0;j<npredicates;j++) {
00211         f_prf.print(" (|lt"+n+"| \"\" (GRIND) (SKIP) (SKIP))\n");
00212         n++;
00213         f_prf.print(" (|lt"+n+"| \"\" (GRIND) (SKIP) (SKIP))\n");
00214         n++;
00215       }
00216 
00217 
00218   n=1;
00219   for(i=0;i<npredicates;i++)
00220     for(j=0;j<npredicates;j++) {
00221         f_prf.print(" (|gt"+n+"| \"\" (GRIND) (SKIP) (SKIP))\n");
00222         n++;
00223         f_prf.print(" (|gt"+n+"| \"\" (GRIND) (SKIP) (SKIP))\n");
00224         n++;
00225       }
00226 
00227 
00228 
00229   f_prf.print(")");
00230   
00231  } 
00232 /* reads the output of PVS in a vector */
00233  public static Vector read(InputStream is) {
00234     try {
00235         BufferedReader r = new BufferedReader( new InputStreamReader(is));
00236     String line = r.readLine();
00237         Vector v = new Vector();
00238         
00239         while(line != null) {
00240       StringTokenizer st = new StringTokenizer(line);
00241       while (st.hasMoreTokens()) {
00242                String s = st.nextToken();
00243            if(s.compareTo("proved")==0) 
00244          v.add( new Integer(1)); 
00245            if(s.compareTo("unproved")==0)
00246                  v.add( new Integer(0)); 
00247           }
00248       line = r.readLine();
00249         }
00250         r.close();
00251         return v;       
00252     } catch (Exception e) {
00253         e.printStackTrace();
00254     throw new RuntimeException("could not read output from pvs\n");
00255     }
00256  } 
00257 /* builds the rest of the pvs theory */
00258  public static void rest(PrintWriter f_pvs, int npredicates, int basic_type) {
00259 
00260   int n; /* theorem number */
00261   int i,j,k;
00262 
00263   /* for each operation generate all the possible combinations 
00264      given by npredicates */
00265 
00266 
00267   f_pvs.println("\n");
00268 
00269   n=1;
00270   for(i=0;i<npredicates;i++)
00271     for(j=0;j<npredicates;j++)
00272       for(k=0;k<npredicates;k++) {
00273         f_pvs.print(" add"+n+": THEOREM ((P"+i+"(e1) AND P"+j+"(e2)) IMPLIES NOT P"+k+"(e1+e2))\n");
00274         n++;
00275       } 
00276 
00277   f_pvs.print("\n");
00278   n=1;
00279   for(i=0;i<npredicates;i++)
00280     for(j=0;j<npredicates;j++)
00281       for(k=0;k<npredicates;k++) {
00282         f_pvs.print(" sub"+n+": THEOREM ((P"+i+"(e1) AND P"+j+"(e2)) IMPLIES NOT P"+k+"(e1-e2))\n");
00283         n++;
00284       }
00285 
00286   f_pvs.print("\n");
00287   n=1;
00288   for(i=0;i<npredicates;i++)
00289     for(j=0;j<npredicates;j++)
00290       for(k=0;k<npredicates;k++) {
00291         f_pvs.print(" mul"+n+": THEOREM ((P"+i+"(e1) AND P"+j+"(e2)) IMPLIES NOT P"+k+"(e1*e2))\n");
00292         n++;
00293       }
00294 
00295   f_pvs.print("\n");
00296   n=1;
00297   for(i=0;i<npredicates;i++)
00298     for(j=0;j<npredicates;j++)
00299       for(k=0;k<npredicates;k++) {
00300         f_pvs.print(" div"+n+": THEOREM ((P"+i+"(e1) AND P"+j+"(nz_e)) IMPLIES NOT P"+k+"(e1/nz_e))\n");
00301         n++;
00302       }
00303 
00304   if(basic_type==sym.INT) {
00305   f_pvs.print("\n");
00306   n=1;
00307   for(i=0;i<npredicates;i++)
00308     for(j=0;j<npredicates;j++)
00309       for(k=0;k<npredicates;k++) {
00310         f_pvs.print(" rem"+n+": THEOREM ((P"+i+"(e1) AND P"+j+"(nz_e)) IMPLIES NOT P"+k+"(e1//nz_e))\n");
00311         n++;
00312       }
00313   }
00314   f_pvs.print("\n");
00315   n=1;
00316   for(i=0;i<npredicates;i++)
00317     for(j=0;j<npredicates;j++) {
00318         f_pvs.print(" eq"+n+": THEOREM ((P"+i+"(e1) AND P"+j+"(e2)) IMPLIES NOT TRUE?(e1=e2))\n"); n++;
00319         f_pvs.print(" eq"+n+": THEOREM ((P"+i+"(e1) AND P"+j+"(e2)) IMPLIES NOT FALSE?(e1=e2))\n");
00320         n++;
00321       }
00322 
00323 
00324 
00325   f_pvs.print("\n");
00326   n=1;
00327   for(i=0;i<npredicates;i++)
00328     for(j=0;j<npredicates;j++) {
00329         f_pvs.print(" lt"+n+": THEOREM ((P"+i+"(e1) AND P"+j+"(e2)) IMPLIES NOT TRUE?(e1<e2))\n"); n++;
00330         f_pvs.print(" lt"+n+": THEOREM ((P"+i+"(e1) AND P"+j+"(e2)) IMPLIES NOT FALSE?(e1<e2))\n");
00331         n++;
00332       }
00333 
00334 
00335 
00336   f_pvs.print("\n");
00337   n=1;
00338   for(i=0;i<npredicates;i++)
00339     for(j=0;j<npredicates;j++) {
00340         f_pvs.print(" gt"+n+": THEOREM ((P"+i+"(e1) AND P"+j+"(e2)) IMPLIES NOT TRUE?(e1>e2))\n"); n++;
00341         f_pvs.print(" gt"+n+": THEOREM ((P"+i+"(e1) AND P"+j+"(e2)) IMPLIES NOT FALSE?(e1>e2))\n");
00342         n++;
00343       }
00344 
00345 
00346   f_pvs.println("END abstraction");
00347 
00348  } 
00349 /* writes ops in abstraction f_spec file */
00350  public static void rest_BASL(PrintWriter f_spec, int npredicates, 
00351                   int basic_type, Vector tokens) {
00352     int n,i,j,k,flag,m;
00353 
00354     Vector v;
00355         int value; /* 1 = TRUE, 2 = FALSE, 0 = T */
00356 
00357         try {
00358     
00359     n=npredicates+2; /* ignore first npredicates+2 proofs from check */
00360 
00361         int lookahead=((Integer)proofs.elementAt(n)).intValue();
00362 
00363     /* generate code for add */
00364     f_spec.print(" operator + add\n  begin\n");
00365     for(i=0;i<npredicates;i++)
00366           for(j=0;j<npredicates;j++) {
00367             f_spec.print("   ("+tokens.elementAt(i)+" , "+tokens.elementAt(j)+
00368              ") -> ");flag=0;
00369             for(k=0;k<npredicates;k++) {
00370               if(lookahead==0) /* UNPROVED */ {
00371                 if(flag==0) {f_spec.print("{");flag=1;}
00372                 else f_spec.print(",");
00373                 f_spec.print(" "+tokens.elementAt(k)+" ");
00374               }
00375               n++; lookahead=((Integer)proofs.elementAt(n)).intValue();
00376             }
00377             if (flag==0) f_spec.print(" T; /* ERROR */\n");
00378             else f_spec.print("};\n");
00379           } 
00380         f_spec.print("  end\n\n");
00381 
00382         /* generate code for sub */
00383     f_spec.print(" operator - sub\n  begin\n");
00384     for(i=0;i<npredicates;i++)
00385           for(j=0;j<npredicates;j++) {
00386             f_spec.print("   ("+tokens.elementAt(i)+" , "+tokens.elementAt(j)+
00387              ") -> ");flag=0;
00388             for(k=0;k<npredicates;k++) {
00389               if(lookahead==0) /* UNPROVED */ {
00390                 if(flag==0) {f_spec.print("{");flag=1;}
00391                 else f_spec.print(",");
00392                 f_spec.print(" "+tokens.elementAt(k)+" ");
00393               }
00394               n++; lookahead=((Integer)proofs.elementAt(n)).intValue();
00395             }
00396             if (flag==0) f_spec.print(" T; /* ERROR */\n");
00397             else f_spec.print("};\n");
00398           } 
00399         f_spec.print("  end\n\n");
00400 
00401     /* generate code for mul */
00402     f_spec.print(" operator * mul\n  begin\n");
00403     for(i=0;i<npredicates;i++)
00404           for(j=0;j<npredicates;j++) {
00405             f_spec.print("   ("+tokens.elementAt(i)+" , "+tokens.elementAt(j)+
00406              ") -> ");flag=0;
00407             for(k=0;k<npredicates;k++) {
00408               if(lookahead==0) /* UNPROVED */ {
00409                 if(flag==0) {f_spec.print("{");flag=1;}
00410                 else f_spec.print(",");
00411                 f_spec.print(" "+tokens.elementAt(k)+" ");
00412               }
00413               n++; lookahead=((Integer)proofs.elementAt(n)).intValue();
00414             }
00415             if (flag==0) f_spec.print(" T; /* ERROR */\n");
00416             else f_spec.print("};\n");
00417           } 
00418         f_spec.print("  end\n\n");
00419 
00420     
00421         /* generate code for div */
00422     f_spec.print(" operator / div\n  begin\n");
00423     for(i=0;i<npredicates;i++)
00424           for(j=0;j<npredicates;j++) {
00425             f_spec.print("   ("+tokens.elementAt(i)+" , "+tokens.elementAt(j)+
00426              ") -> ");flag=0;
00427             for(k=0;k<npredicates;k++) {
00428               if(lookahead==0) /* UNPROVED */ {
00429                 if(flag==0) {f_spec.print("{");flag=1;}
00430                 else f_spec.print(",");
00431                 f_spec.print(" "+tokens.elementAt(k)+" ");
00432               }
00433               n++; lookahead=((Integer)proofs.elementAt(n)).intValue();
00434             }
00435             if (flag==0) f_spec.print(" T; /* ERROR */\n");
00436             else f_spec.print("};\n");
00437           } 
00438         f_spec.print("  end\n\n");
00439 
00440     if(basic_type == sym.INT) {
00441     /* generate code for rem */
00442     f_spec.print(" operator % rem\n  begin\n");
00443     for(i=0;i<npredicates;i++)
00444           for(j=0;j<npredicates;j++) {
00445             f_spec.print("   ("+tokens.elementAt(i)+" , "+tokens.elementAt(j)+
00446              ") -> ");flag=0;
00447             for(k=0;k<npredicates;k++) {
00448               if(lookahead==0) /* UNPROVED */ {
00449                 if(flag==0) {f_spec.print("{");flag=1;}
00450                 else f_spec.print(",");
00451                 f_spec.print(" "+tokens.elementAt(k)+" ");
00452               }
00453               n++; lookahead=((Integer)proofs.elementAt(n)).intValue();
00454             }
00455             if (flag==0) f_spec.print(" T; /* ERROR */\n");
00456             else f_spec.print("};\n");
00457           } 
00458         f_spec.print("  end\n\n");
00459     }
00460 
00461 
00462     
00463     v = new Vector();
00464     /* generate code for eq */
00465     f_spec.print(" test == eq\n  begin\n");
00466     for(i=0;i<npredicates;i++)
00467           for(j=0;j<npredicates;j++) {
00468 
00469         value = 0;
00470 
00471             f_spec.print("   ("+tokens.elementAt(i)+" , "+tokens.elementAt(j)+
00472              ") -> ");flag=0;
00473             if(lookahead==0) /* UNPROVED */ {
00474                 if(flag==0) {f_spec.print("{");flag=1;}
00475                 else f_spec.print(",");
00476                 f_spec.print(" TRUE ");
00477 
00478         value = 1;
00479 
00480               }
00481             n++; lookahead=((Integer)proofs.elementAt(n)).intValue();
00482             if(lookahead==0) /* UNPROVED */ {
00483                 if(flag==0) {f_spec.print("{");flag=1;}
00484                 else f_spec.print(",");
00485                 f_spec.print(" FALSE ");
00486 
00487         if(value==1) value=0; else value=2;
00488 
00489               }
00490             n++; lookahead=((Integer)proofs.elementAt(n)).intValue();            
00491 
00492             if (flag==0) f_spec.print(" T; /* ERROR */\n");
00493             else f_spec.print("};\n");
00494 
00495         v.add( new Integer(value));
00496 
00497           } 
00498         f_spec.print("  end\n\n");
00499 
00500     /* generate code for neq */
00501     m =0;
00502     f_spec.print(" test != neq\n  begin\n");
00503     for(i=0;i<npredicates;i++)
00504           for(j=0;j<npredicates;j++) {
00505             f_spec.print("   ("+tokens.elementAt(i)+" , "+tokens.elementAt(j)+
00506              ") -> ");
00507 
00508         value = ((Integer)v.elementAt(m)).intValue();m++;
00509             if(value==0) /* T */ 
00510           f_spec.print("{ TRUE , FALSE };\n");
00511         if(value==1) /* TRUE */
00512           f_spec.print("{ FALSE };\n");
00513         if(value==2) /* FALSE */
00514           f_spec.print("{ TRUE };\n");
00515           }    
00516         f_spec.print("  end\n\n");
00517 
00518         v = new Vector();
00519     /* generate code for lt */
00520     f_spec.print(" test < lt\n  begin\n");
00521     for(i=0;i<npredicates;i++)
00522           for(j=0;j<npredicates;j++) {
00523 
00524         value = 0;
00525 
00526             f_spec.print("   ("+tokens.elementAt(i)+" , "+tokens.elementAt(j)+
00527              ") -> ");flag=0;
00528             if(lookahead==0) /* UNPROVED */ {
00529                 if(flag==0) {f_spec.print("{");flag=1;}
00530                 else f_spec.print(",");
00531                 f_spec.print(" TRUE ");
00532 
00533         value = 1;
00534 
00535               }
00536             n++; lookahead=((Integer)proofs.elementAt(n)).intValue();
00537             if(lookahead==0) /* UNPROVED */ {
00538                 if(flag==0) {f_spec.print("{");flag=1;}
00539                 else f_spec.print(",");
00540                 f_spec.print(" FALSE ");
00541 
00542         if(value==1) value=0; else value=2;
00543 
00544               }
00545             n++; lookahead=((Integer)proofs.elementAt(n)).intValue();            
00546 
00547             if (flag==0) f_spec.print(" T; /* ERROR */\n");
00548             else f_spec.print("};\n");
00549 
00550         v.add( new Integer(value));
00551           } 
00552         f_spec.print("  end\n\n");
00553 
00554         /* generate code for ge */
00555     m =0;
00556     f_spec.print(" test >= ge\n  begin\n");
00557     for(i=0;i<npredicates;i++)
00558           for(j=0;j<npredicates;j++) {
00559             f_spec.print("   ("+tokens.elementAt(i)+" , "+tokens.elementAt(j)+
00560              ") -> ");
00561 
00562         value = ((Integer)v.elementAt(m)).intValue();m++;
00563             if(value==0) /* T */ 
00564           f_spec.print("{ TRUE , FALSE };\n");
00565         if(value==1) /* TRUE */
00566           f_spec.print("{ FALSE };\n");
00567         if(value==2) /* FALSE */
00568           f_spec.print("{ TRUE };\n");
00569           }     
00570         f_spec.print("  end\n\n");
00571 
00572         v = new Vector();
00573     /* generate code for gt */
00574     f_spec.print(" test > gt\n  begin\n");
00575     for(i=0;i<npredicates;i++)
00576           for(j=0;j<npredicates;j++) {
00577 
00578         value = 0;
00579 
00580             f_spec.print("   ("+tokens.elementAt(i)+" , "+tokens.elementAt(j)+
00581              ") -> ");flag=0;
00582             if(lookahead==0) /* UNPROVED */ {
00583                 if(flag==0) {f_spec.print("{");flag=1;}
00584                 else f_spec.print(",");
00585                 f_spec.print(" TRUE ");
00586 
00587         value = 1;
00588 
00589               }
00590             n++; lookahead=((Integer)proofs.elementAt(n)).intValue();
00591             if(lookahead==0) /* UNPROVED */ {
00592                 if(flag==0) {f_spec.print("{");flag=1;}
00593                 else f_spec.print(",");
00594                 f_spec.print(" FALSE ");
00595 
00596         if(value==1) value=0; else value=2;
00597 
00598               }
00599             n++; lookahead=((Integer)proofs.elementAt(n)).intValue();            
00600 
00601             if (flag==0) f_spec.print(" T; /* ERROR */\n");
00602             else f_spec.print("};\n");
00603 
00604         v.add( new Integer(value));
00605           } 
00606         f_spec.print("  end\n\n");
00607 
00608         /* generate code for le */
00609     m =0;
00610     f_spec.print(" test <= le\n  begin\n");
00611     for(i=0;i<npredicates;i++)
00612           for(j=0;j<npredicates;j++) {
00613             f_spec.print("   ("+tokens.elementAt(i)+" , "+tokens.elementAt(j)+
00614              ") -> ");
00615 
00616         value = ((Integer)v.elementAt(m)).intValue();m++;
00617             if(value==0) /* T */ 
00618           f_spec.print("{ TRUE , FALSE };\n");
00619         if(value==1) /* TRUE */
00620           f_spec.print("{ FALSE };\n");
00621         if(value==2) /* FALSE */
00622           f_spec.print("{ TRUE };\n");
00623           }     
00624         f_spec.print("  end\n\n");
00625 
00626         f_spec.print(" end\n");
00627 
00628          } catch (Exception e) {
00629             e.printStackTrace();
00630              throw new 
00631          RuntimeException("could not generate spec file from pvs output");
00632          }
00633 
00634  } 
00635 }
Generated at Thu Feb 7 06:53:12 2002 for Bandera by doxygen1.2.10 written by Dimitri van Heesch, © 1997-2001