SpeAR 2.1.1

This release introduces SpeAR 2.1.1. This release introduces several improvements to the underlying tool to improve efficiency, readability, and maintainability of the code. This release does not introduce any new features. Any feedback on errors/issues should be reported as issues here.

---

SpeAR requires an SMT solver to be installed to work correctly. SMTInterpol is bundled with SpeAR and will support logical entailment and logical consistency analysis. Z3 is strongly recommended and is required to run realizability analysis.

SpeAR also supports the following solvers for logical entailment and logical consistency analysis.
- CVC4
- Yices2

The solver that JKind uses for its analyses can be set from the Window -> Preferences, SpeAR Menu.

Lastly, the feature for generating graphical representations of a specification requires GraphViz to be installed.

SpeAR 2.1.0

This release introduces SpeAR 2.1.0. This release introduces several new features, that have been well-tested since the previous beta release. The core functionality of SpeAR remains unchanged from version 2.0.0 or 2.1.0 beta. Any feedback on errors/issues should be reported as issues here.

Features added in this release include:

• Unique First Cause test generation for basic logical operators
  • just add ufc between the ID and colon of any requirement or behavior
  • i.e. r0 ufc: a and b
• Promotion of several operators to first-class citizens of the language
  • a responds to b (within N steps)
  • a precedes b
  • count a (counts how many times a boolean is true)
  • ccount a (counts how many times a boolean has been consecutively true)
  • btoi a (converts a boolean to an integer, 1 for true, 0 for false)
• Introduction of set expressions
  • a set of elements {a, b, c, d}
  • an interval {a .. b}
• Introduction of an in expression to check set membership
  • x in {a,b,c,d} (equivalent to x == a or x == b or x == c or x == d)
  • x in y (where y is an array)
  • x in [a, b, c, d] (equivalent to x == a or x == b or x == c or x == d)
  • x in {a .. b} (equivalent to x > a and x < b)
• Batch analysis capability
• A command line interface

Some changes from previous versions:

• disabling unused variable validations also disables check for uninitialized previous operators
• arrow operators are now allowed inside of specifications, previously they were only allowed inside of pattern bodies

Operators that are supported for UFC test generation

• and
• or
• xor
• not
• implies
• previous
• arrow (->)
• xor
• if/then/else
• relational operators (>, >=, <, <=, ==, <>)

---

SpeAR requires an SMT solver to be installed to work correctly. SMTInterpol is bundled with SpeAR and will support logical entailment and logical consistency analysis. Z3 is strongly recommended and is required to run realizability analysis.

SpeAR also supports the following solvers for logical entailment and logical consistency analysis.
- CVC4
- Yices2

The solver that JKind uses for its analyses can be set from the Window -> Preferences, SpeAR Menu.

Lastly, the feature for generating graphical representations of a specification requires GraphViz to be installed.

SpeAR 2.1.0 beta

This release introduces SpeAR 2.1.0 beta. This release introduces several new features that are in a beta stage. The core functionality of SpeAR remains unchanged from version 2.0.0 Any feedback on errors/issues should be reported as issues here.

Features added in this release include:

• Unique First Cause test generation for basic logical operators
  • just add ufc between the ID and colon of any requirement or behavior
  • i.e. r0 ufc: a and b
• Promotion of several operators to first-class citizens of the language
  • a responds to b (within N steps)
  • a precedes b
  • count a (counts how many times a boolean is true)
  • ccount a (counts how many times a boolean has been consecutively true)
  • btoi a (converts a boolean to an integer, 1 for true, 0 for false)
• Introduction of set expressions
  • a set of elements {a, b, c, d}
  • an interval {a .. b}
• Introduction of an in expression to check set membership
  • x in {a,b,c,d}
  • x in y (where y is an array)
  • x in [a, b, c, d]
• Batch analysis capability
• A command line interface

Some changes from previous versions:

• disabling unused variable validations also disables check for uninitialized previous operators
• arrow operators are now allowed inside of specifications, previously they were only allowed inside of pattern bodies

Operators that are supported for UFC test generation

• and
• or
• xor
• not
• implies
• previous
• arrow (->)
• xor
• if/then/else
• relational operators (>, >=, <, <=, ==, <>)

This release also includes a case study that shows how SpeAR can be used to satisfy DO-178C objectives. Check the "s5" project in the release binary.

---

SpeAR requires an SMT solver to be installed to work correctly. SMTInterpol is bundled with SpeAR and will support logical entailment and logical consistency analysis. Z3 is strongly recommended and is required to run realizability analysis.

SpeAR also supports the following solvers for logical entailment and logical consistency analysis.
- CVC4
- Yices 2

The solver that JKind uses for its analyses can be set from the Window -> Preferences, SpeAR Menu.

Lastly, the feature for generating graphical representations of a specification requires GraphViz to be installed.

SpeAR 2.0.0

This release introduces SpeAR 2.0.0. This release candidate is a fully featured version of SpeAR. Any feedback on errors/issues should be reported as issues here.

SpeAR requires an SMT solver to be installed to work correctly. SMTInterpol is bundled with SpeAR and will support logical entailment and logical consistency analysis. Z3 is strongly recommended and is required to run realizability analysis.

SpeAR also supports the following solvers for logical entailment and logical consistency analysis.
- CVC4
- Yices 2

The solver that JKind uses for its analyses can be set from the Window -> Preferences, SpeAR Menu.

Lastly, the feature for generating graphical representations of a specification requires GraphViz to be installed.

SpeAR Release Candidate 21

This release introduces SpeAR 2.0 release candidate 21. This release candidate is a fully featured version of SpeAR 2.0. Any feedback on errors/issues should be reported as issues here.

This release adds the traceability matrix for logical entailment analysis when the IVC flag is set. After setting the IVC flag in the preferences tab, users can view which requirements were necessary to prove which properties by right clicking and viewing the traceability matrix. In addition, a property that produces the conjunct of all the properties is also provided.

This release also adds many bugfixes, internal optimizations, tweaks to the Preferences UI, and minor refactoring improvements that are too numerous to be listed here.

General Information:

SpeAR requires an SMT solver to be installed to work correctly. SMTInterpol is bundled with SpeAR and will support logical entailment and logical consistency analysis. Z3 is strongly recommended and is required to run realizability analysis.

SpeAR also supports the following solvers for logical entailment and logical consistency analysis.
- CVC4
- Yices 2

The solver that JKind uses for its analyses can be set from the Window -> Preferences, SpeAR Menu.

Lastly, the feature for generating graphical representations of a specification requires GraphViz to be installed.

Enjoy.

SpeAR Release Candidate 20

This release introduces SpeAR 2.0 release candidate 20. This release candidate is a fully featured version of SpeAR 2.0. Any feedback on errors/issues should be reported as issues here.

This release introduces support for:

• real to integer casting (rounding mode of floor supported only) #74
• integer to real casting #74
• modulus for reals (supported by Z3 solver only) #73

The following screenshot shows an example of each:

Finally, this release resolves issues: #66, #68, and #69.

General Information:

SpeAR requires an SMT solver to be installed to work correctly. SMTInterpol is bundled with SpeAR and will support logical entailment and logical consistency analysis. Z3 is strongly recommended and is required to run realizability analysis.

SpeAR also supports the following solvers for logical entailment and logical consistency analysis.
- CVC4
- Yices 2

The solver that JKind uses for its analyses can be set from the Window -> Preferences, SpeAR Menu.

Lastly, the feature for generating graphical representations of a specification requires GraphViz to be installed.

Enjoy.

SpeAR Release Candidate 19

#Current Release Information

This release introduces SpeAR 2.0 release candidate 19. This release candidate is a fully featured version of SpeAR 2.0. Any feedback on errors/issues should be reported as issues here.

This release introduces predicate subtypes. Predicate subtypes are powerful expressive types that will make the SpeAR specifications much more concise. See the example below for several examples on how to write and interpret predicate subtypes.

Predicate subtypes can be vacuous if incorrectly specified. Here is an example of an obviously vacuous type.

Every type can be checked by right clicking on it in the editor and selecting "Check Type Validity." If a type is valid (it has at least one value that fulfills the underlying predicates) it will appear as a green check box. If a type is invalid (it has no satisfying values) it will appear as red exclamation point.

The result for the vacuous type shown above is:

---

General Information:

SpeAR requires an SMT solver to be installed to work correctly. SMTInterpol is bundled with SpeAR and will support logical entailment and logical consistency analysis. Z3 is strongly recommended and is required to run realizability analysis.

SpeAR also supports the following solvers for logical entailment and logical consistency analysis.
- CVC4
- Yices 2

The solver that JKind uses for its analyses can be set from the Window -> Preferences, SpeAR Menu.

Lastly, the feature for generating graphical representations of a specification requires GraphViz to be installed.

Enjoy.

SpeAR Release Candidate 18

This release introduces SpeAR 2.0 release candidate 18. This release candidate is a fully featured version of SpeAR 2.0. Any feedback on errors/issues should be reported as issues here.

This release introduces the Excel export feature of SpeAR. This feature will create an export of SpeAR requirements using the data fields introduced in Release Candidate 14. Traceability is established using the "trace" data element. More information can be found in the release example, /export/Sys_Top_Level.spear and /export/Sub_Sys_A.spear. The Excel output feature can be executed by selecting the SpeAR menu -> Generate Excel:

Users should note that they must have a program installed to view Excel spreadsheets to use this feature. Thank you to @janetlj for implementing this feature.

This release also includes a more concise Preferences page. This page removes all of the non-JKind model checker preferences as the JKind model checker is now embedded in each release of SpeAR. The new preferences menu now appears like this:

Finally, this release fixes Issue #64. Thank you to @manthonyaiello for identifying this issue, and many like it. Your help is greatly appreciated.

SpeAR requires an SMT solver to be installed to work correctly. SMTInterpol is bundled with SpeAR and will support logical entailment and logical consistency analysis. Z3 is strongly recommended and is required to run realizability analysis.

SpeAR also supports the following solvers for logical entailment and logical consistency analysis.
- CVC4
- Yices 2

The solver that JKind uses for its analyses can be set from the Window -> Preferences, SpeAR Menu.

Lastly, the feature for generating graphical representations of a specification requires GraphViz to be installed.

Enjoy.

SpeAR Release Candidate 17

This release introduces SpeAR 2.0 release candidate 17. This release candidate is a fully featured version of SpeAR 2.0. Any feedback on errors/issues should be reported as issues here.

This version provides an option to turn off IVC analysis during logical entailment, which provides the traceability information on which requirements were needed to prove which properties. This flag is shown below:

Disabling this flag should improve property checking times, if the user is not interested in the traceability features. This release also addresses #62.

SpeAR requires an SMT solver to be installed to work correctly. SMTInterpol is bundled with SpeAR and will support logical entailment and logical consistency analysis. Z3 is strongly recommended and is required to run realizability analysis.

SpeAR also supports the following solvers for logical entailment and logical consistency analysis.
- CVC4
- Yices 2

The solver that JKind uses for its analyses can be set from the Window -> Preferences, SpeAR Menu.

Lastly, the feature for generating graphical representations of a specification requires GraphViz to be installed.

Enjoy.

SpeAR RC 16

This release introduces SpeAR 2.0 release candidate 16.

This release candidate is a fully featured version of SpeAR 2.0. Any feedback on errors/issues should be reported as issues here.

This version introduces a capability to generate a graphical representation of a SpeAR spec. This representation shows the call hierarchy from the top level specification. The user can select (via the Window -> Preferences, SpeAR Menu option) to generate a fully recursive graph or just one for the current level. The graphical representation requires GraphViz to be installed to work correctly.

Graphical representations use ellipses to represent specifications, rectangles to represent definitions files, and hexagons to represent patterns. Consider the following example of four specifications, where specification "main" is the top level spec:

Using this capability a user can generate a graphical representation for any specification and its direct calls by generating a graph with the recursive graph option unselected. The resulting graph for the "main" specification shown above is:

Otherwise, the user can generate a fully recursive graph by turning the option on. The resulting graph from doing that is:

SpeAR requires an SMT solver to be installed to work correctly. SMTInterpol is bundled with SpeAR and will support logical entailment and logical consistency analysis. Z3 is strongly recommended and is required to run realizability analysis.

SpeAR also supports the following solvers for logical entailment and logical consistency analysis.
- CVC4
- Yices 2

The solver that JKind uses for its analyses can be set from the Window -> Preferences, SpeAR Menu.

Lastly, the feature for generating graphical representations of a specification requires GraphViz to be installed.

Enjoy.