001 package daikon.inv;
002 import daikon.*;
003 import utilMDE.Pair;
004 import java.util.*;
005
006 /**
007 * Enumeration type for output style.
008 * (Should this be somewhere else?)
009 **/
010 public enum OutputFormat {
011
012 /** The standard, concise Daikon output format */
013 DAIKON("Daikon"),
014 /** Design-By-Contract for Java (used by Parasoft JContract) */
015 DBCJAVA("DBC") {
016 public String ensures_tag() { return "@post"; }
017 public String requires_tag() { return "@pre"; }
018 },
019 /** ESC/Java's annotation language */
020 ESCJAVA("ESC/Java"),
021 /** Java boolean expression */
022 JAVA("Java"),
023 /** Java Modeling Language */
024 JML("JML"),
025 /** Simplify theorem prover */
026 SIMPLIFY("Simplify");
027
028 String name;
029
030 OutputFormat(String name) { this.name = name; }
031
032 public String toString() { return "OutputFormat:" + name; }
033
034 public boolean isJavaFamily() {
035 return (this == DBCJAVA || this == JML || this == JAVA);
036 }
037
038 // We define the get() method instead of using valueOf() because get()
039 // can be case-sensitive, can permit alternative names, etc. An enum
040 // cannot override valueOf().
041 /**
042 * Return the appropriate OutputFormat for the given name, or null
043 * if no such OutputFormat exists.
044 **/
045 public static OutputFormat get(String name) {
046 // if (name == null) { return null; }
047 if (name.compareToIgnoreCase(DAIKON.name) == 0) { return DAIKON; }
048 if (name.compareToIgnoreCase(DBCJAVA.name) == 0) { return DBCJAVA; }
049 if (name.compareToIgnoreCase(ESCJAVA.name) == 0) { return ESCJAVA; }
050 if (name.compareToIgnoreCase("ESC") == 0) { return ESCJAVA; }
051 if (name.compareToIgnoreCase(JAVA.name) == 0) { return JAVA; }
052 if (name.compareToIgnoreCase(JML.name) == 0) { return JML; }
053 if (name.compareToIgnoreCase(SIMPLIFY.name) == 0) { return SIMPLIFY; }
054 // return null;
055 throw new Error("Unknown OutputFormat " + name);
056 }
057
058 public String ensures_tag() { return "ensures"; }
059 public String requires_tag() { return "requires"; }
060
061 }