001package daikon.inv;
002
003import org.checkerframework.checker.lock.qual.GuardSatisfied;
004import org.checkerframework.dataflow.qual.Pure;
005import org.checkerframework.dataflow.qual.SideEffectFree;
006
007/** Enumeration type for output style. (Should this be somewhere else?) */
008public enum OutputFormat {
009
010  /** The standard, concise Daikon output format. Intended to be read by humans. */
011  DAIKON("Daikon"),
012  /** Design-By-Contract for Java (used by Parasoft JContract) */
013  DBCJAVA("DBC") {
014    @Override
015    public String ensures_tag() {
016      return "@post";
017    }
018
019    @Override
020    public String requires_tag() {
021      return "@pre";
022    }
023  },
024  /** ESC/Java's annotation language -- a variant of JML. */
025  ESCJAVA("ESC/Java"),
026  /** Java boolean expression. */
027  JAVA("Java"),
028  /** Java Modeling Language. */
029  JML("JML"),
030  /** Simplify theorem prover. First order logical expressions, expressed in Lisp-style parens. */
031  SIMPLIFY("Simplify"),
032  /** C# Code Contract. */
033  CSHARPCONTRACT("CSharpContract");
034
035  final String name;
036
037  OutputFormat(String name) {
038    this.name = name;
039  }
040
041  @SideEffectFree
042  @Override
043  public String toString(@GuardSatisfied OutputFormat this) {
044    return "OutputFormat:" + name;
045  }
046
047  @Pure
048  public boolean isJavaFamily() {
049    return (this == DBCJAVA || this == JML || this == JAVA);
050  }
051
052  // We define the get() method instead of using valueOf() because get()
053  // can be case-sensitive, can permit alternative names, etc.  An enum
054  // cannot override valueOf().
055  /**
056   * Return the appropriate OutputFormat for the given name, or throw an error if no such
057   * OutputFormat exists.
058   */
059  public static OutputFormat get(String name) {
060    // if (name == null) { return null; }
061    if (name.compareToIgnoreCase(DAIKON.name) == 0) {
062      return DAIKON;
063    }
064    if (name.compareToIgnoreCase(DBCJAVA.name) == 0) {
065      return DBCJAVA;
066    }
067    if (name.compareToIgnoreCase(ESCJAVA.name) == 0) {
068      return ESCJAVA;
069    }
070    if (name.compareToIgnoreCase("ESC") == 0) {
071      return ESCJAVA;
072    }
073    if (name.compareToIgnoreCase(JAVA.name) == 0) {
074      return JAVA;
075    }
076    if (name.compareToIgnoreCase(JML.name) == 0) {
077      return JML;
078    }
079    if (name.compareToIgnoreCase(SIMPLIFY.name) == 0) {
080      return SIMPLIFY;
081    }
082    if (name.compareToIgnoreCase(CSHARPCONTRACT.name) == 0) {
083      return CSHARPCONTRACT;
084    }
085    // return null;
086    throw new Error("Unknown OutputFormat " + name);
087  }
088
089  public String ensures_tag() {
090    return "ensures";
091  }
092
093  public String requires_tag() {
094    return "requires";
095  }
096}