Apply corrections suggested by @akullpp
This commit is contained in:
13
README.md
13
README.md
@ -101,7 +101,6 @@ A curated list of awesome Java frameworks, libraries and software.
|
|||||||
## Code Analysis
|
## Code Analysis
|
||||||
|
|
||||||
*Tools that provide metrics and quality measurements.*
|
*Tools that provide metrics and quality measurements.*
|
||||||
* [Checker Framework](http://types.cs.washington.edu/checker-framework/) - Enhances Java’s type system to make it more powerful and useful.
|
|
||||||
* [Checkstyle](https://github.com/checkstyle/checkstyle) - Static analysis of coding conventions and standards.
|
* [Checkstyle](https://github.com/checkstyle/checkstyle) - Static analysis of coding conventions and standards.
|
||||||
* [Error Prone](https://github.com/google/error-prone) - Catches common programming mistakes as compile-time errors.
|
* [Error Prone](https://github.com/google/error-prone) - Catches common programming mistakes as compile-time errors.
|
||||||
* [FindBugs](http://findbugs.sourceforge.net/) - Static analysis of bytecode to find potential bugs.
|
* [FindBugs](http://findbugs.sourceforge.net/) - Static analysis of bytecode to find potential bugs.
|
||||||
@ -255,13 +254,15 @@ A curated list of awesome Java frameworks, libraries and software.
|
|||||||
|
|
||||||
*Formal-methods tools: proof assistants, model checking, symbolic execution etc.*
|
*Formal-methods tools: proof assistants, model checking, symbolic execution etc.*
|
||||||
|
|
||||||
* [Daikon](http://plse.cs.washington.edu/daikon/) - Daikon is an implementation of dynamic detection of likely invariants; that is, the Daikon invariant detector reports likely program invariants. Can generate JML specs based on the invariants.
|
* [CATG](https://github.com/ksen007/janala2) - A concolic unit testing engine for Java programs. Automatically generates unit tests for Java programs using formal methods.
|
||||||
|
* [Checker Framework](http://types.cs.washington.edu/checker-framework/) - Pluggable type systems for Java. Includes nullness types, physical units, immutability types and more.
|
||||||
|
* [Daikon](http://plse.cs.washington.edu/daikon/) - Daikon detects likely program invariants and can generate JML specs based on those invariats.
|
||||||
* [Java Modeling Language (JML)](http://www.jmlspecs.org) - A behavioral interface specification language that can be used to specify the behavior of Java modules. It combines the design by contract approach of Eiffel and the model-based specification approach of the Larch family of interface specification languages, with some elements of the refinement calculus. Used by several other Java verification tools.
|
* [Java Modeling Language (JML)](http://www.jmlspecs.org) - A behavioral interface specification language that can be used to specify the behavior of Java modules. It combines the design by contract approach of Eiffel and the model-based specification approach of the Larch family of interface specification languages, with some elements of the refinement calculus. Used by several other Java verification tools.
|
||||||
* [Java Path Finder (JPF)](http://babelfish.arc.nasa.gov/trac/jpf) ([repository](http://babelfish.arc.nasa.gov/hg/jpf/jpf-core/)) - "The Swiss army knife of Java verification." A model checker for Java (bytecode) and more. By NASA
|
* [Java Path Finder (JPF)](http://babelfish.arc.nasa.gov/trac/jpf) - A JVM formal verification tool containing a model checker for Java bytecode and more. Created by NASA.
|
||||||
* [jCUTE](https://github.com/osl/jcute) - The Java Concolic Unit Testing Engine (jCUTE) automatically generates unit tests for Java programs. Concolic execution combines randomized concrete execution with symbolic execution and automatic constraint solving. See also [CATG](https://github.com/ksen007/janala2).
|
* [jCUTE](https://github.com/osl/jcute) - A Java Concolic Unit Testing Engine that automatically generates unit tests for Java programs. Concolic execution combines randomized concrete execution with symbolic execution and automatic constraint solving.
|
||||||
* [JMLOK 2.0](http://massoni.computacao.ufcg.edu.br/home/jmlok) - Setects nonconformances between Java code and JML specification through the feedback-directed random tests generation, and suggests a likely cause for each nonconformance detected
|
* [JMLOK 2.0](http://massoni.computacao.ufcg.edu.br/home/jmlok) - Detects nonconformances between Java code and JML specification through the feedback-directed random tests generation, and suggests a likely cause for each nonconformance detected.
|
||||||
* [KeY](http://key-project.org/) - The KeY System is a formal software development tool that aims to integrate design, implementation, formal specification, and formal verification of object-oriented software as seamlessly as possible. Uses JML for specification and symbolic execution for verification.
|
* [KeY](http://key-project.org/) - The KeY System is a formal software development tool that aims to integrate design, implementation, formal specification, and formal verification of object-oriented software as seamlessly as possible. Uses JML for specification and symbolic execution for verification.
|
||||||
* [OpenJML](http://jmlspecs.sourceforge.net/) ([alternate website](http://openjml.github.io/))- Formal methods tool for Java and the Java Modeling Language (JML). OpenJML translates JML specifications into SMT-LIB format and passes the proof problems implied by the Java+JML program to backend SMT solvers.
|
* [OpenJML](http://openjml.github.io/) - Translates JML specifications into SMT-LIB format and passes the proof problems implied by the program to backend solvers.
|
||||||
|
|
||||||
## Functional Programming
|
## Functional Programming
|
||||||
|
|
||||||
|
Reference in New Issue
Block a user