ESC/Java (original) (raw)
ESC/Java (and more recently ESC/Java2), the "Extended Static Checker for Java," is a programming tool that attempts to find common run-time errors in Java programs at compile time. The underlying approach used in ESC/Java is referred to as extended static checking, which is a collective name referring to a range of techniques for statically checking the correctness of various program constraints. For example, that an integer variable is greater-than-zero, or lies between the bounds of an array. This technique was pioneered in ESC/Java (and its predecessor, ESC/Modula-3) and can be thought of as an extended form of type checking. Extended static checking usually involves the use of an automated theorem prover and, in ESC/Java, the Simplify theorem prover was used.
| Property | Value |
|---|---|
| dbo:abstract | ESC/Java (and more recently ESC/Java2), the "Extended Static Checker for Java," is a programming tool that attempts to find common run-time errors in Java programs at compile time. The underlying approach used in ESC/Java is referred to as extended static checking, which is a collective name referring to a range of techniques for statically checking the correctness of various program constraints. For example, that an integer variable is greater-than-zero, or lies between the bounds of an array. This technique was pioneered in ESC/Java (and its predecessor, ESC/Modula-3) and can be thought of as an extended form of type checking. Extended static checking usually involves the use of an automated theorem prover and, in ESC/Java, the Simplify theorem prover was used. ESC/Java is neither sound nor complete. This was intentional and aims to reduce the number of errors and/or warnings reported to the programmer, in order to make the tool more useful in practice. However, it does mean that: firstly, there are programs that ESC/Java will erroneously consider to be incorrect (known as false-positives); secondly, there are incorrect programs it will consider to be correct (known as false-negatives). Examples in the latter category include errors arising from modular arithmetic and/or multithreading. ESC/Java was originally developed at the Compaq Systems Research Center (SRC). SRC launched the project in 1997, after work on their original extended static checker, ESC/Modula-3, ended in 1996. In 2002, SRC released the source code for ESC/Java and related tools. Recent versions of ESC/Java are based around the Java Modeling Language (JML). Users can control the amount and kinds of checking by annotating their programs with specially formatted comments or pragmas. The University of Nijmegen's Security of Systems group released alpha versions of ESC/Java2, an extended version of ESC/Java that processes the JML specification language through 2004. From 2004 to 2009, ESC/Java2 development was managed by the KindSoftware Research Group at University College Dublin, which in 2009 moved to the IT University of Copenhagen, and in 2012 to the Technical University of Denmark. Over the years, ESC/Java2 has gained many new features including the ability to reason with multiple theorem provers and integration with Eclipse. OpenJML, the successor of ESC/Java2, is available for Java 1.8. The source is available at https://github.com/OpenJML (en) |
| dbo:wikiPageExternalLink | ftp://gatekeeper.dec.com/pub/DEC/SRC/research-reports/abstracts/src-rr-159.html http://www.kindsoftware.com/products/opensource/ESCJava2/ http://www.openjml.org/ https://www.cs.ru.nl/~erikpoll/papers/tfm2009.pdf http://www.hpl.hp.com/downloads/crl/jtk/ https://archive.org/details/formalmethodsfor0000fmco/page/342 https://github.com/OpenJML https://web.archive.org/web/20010228175138/http:/research.compaq.com/SRC/esc/escm3/download.html https://web.archive.org/web/20051208055447/http:/research.compaq.com/SRC/esc/ https://web.archive.org/web/20071002143846/http:/www.researchchannel.org/prog/displayevent.aspx%3FrID=2761 |
| dbo:wikiPageID | 679218 (xsd:integer) |
| dbo:wikiPageLength | 7851 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1065953421 (xsd:integer) |
| dbo:wikiPageWikiLink | dbc:Formal_methods_tools dbr:DEC_Systems_Research_Center dbr:University_College_Dublin dbc:2002_software dbc:Static_program_analysis_tools dbr:Bounds_checking dbr:Modular_arithmetic dbr:Compile_time dbr:Completeness_(logic) dbr:Automated_theorem_proving dbc:Formal_specification_languages dbc:Free_computer_programming_tools dbr:Type_checking dbr:Eclipse_(software) dbr:Directive_(programming) dbr:Source_code dbr:Java_(programming_language) dbr:Technical_University_of_Denmark dbr:Java_Modeling_Language dbr:Automated_theorem_prover dbr:Programming_tool dbr:IT_University_of_Copenhagen dbr:Radboud_University_Nijmegen dbr:Static_code_analysis dbr:Soundness dbr:Extended_static_checking dbr:Run-time_error dbr:Thread_(computer_science) |
| dbp:date | 2001-02-28 (xsd:date) 2005-12-08 (xsd:date) |
| dbp:title | Extended Static Checking Modula-3 (en) Extended Static Checking for Java (en) |
| dbp:url | https://web.archive.org/web/20010228175138/http:/research.compaq.com/SRC/esc/escm3/download.html https://web.archive.org/web/20051208055447/http:/research.compaq.com/SRC/esc/ |
| dbp:wikiPageUsesTemplate | dbt:Cite_conference dbt:More_footnotes dbt:Refbegin dbt:Refend dbt:Reflist dbt:Webarchive |
| dct:subject | dbc:Formal_methods_tools dbc:2002_software dbc:Static_program_analysis_tools dbc:Formal_specification_languages dbc:Free_computer_programming_tools |
| gold:hypernym | dbr:Tool |
| rdf:type | dbo:Software yago:WikicatStaticProgramAnalysisTools yago:Artifact100021939 yago:Implement103563967 yago:Instrumentality103575240 yago:Object100002684 yago:PhysicalEntity100001930 yago:Tool104451818 yago:Whole100003553 yago:WikicatFormalMethodsTools |
| rdfs:comment | ESC/Java (and more recently ESC/Java2), the "Extended Static Checker for Java," is a programming tool that attempts to find common run-time errors in Java programs at compile time. The underlying approach used in ESC/Java is referred to as extended static checking, which is a collective name referring to a range of techniques for statically checking the correctness of various program constraints. For example, that an integer variable is greater-than-zero, or lies between the bounds of an array. This technique was pioneered in ESC/Java (and its predecessor, ESC/Modula-3) and can be thought of as an extended form of type checking. Extended static checking usually involves the use of an automated theorem prover and, in ESC/Java, the Simplify theorem prover was used. (en) |
| rdfs:label | ESC/Java (en) |
| owl:sameAs | freebase:ESC/Java yago-res:ESC/Java wikidata:ESC/Java https://global.dbpedia.org/id/4iShm |
| prov:wasDerivedFrom | wikipedia-en:ESC/Java?oldid=1065953421&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:ESC/Java |
| is dbo:knownFor of | dbr:Greg_Nelson_(computer_scientist) |
| is dbo:wikiPageRedirects of | dbr:ESC/Java2 dbr:Esc_java |
| is dbo:wikiPageWikiLink of | dbr:List_of_computer_scientists dbr:List_of_programmers dbr:Predicate_transformer_semantics dbr:Static_program_analysis dbr:Whiley_(programming_language) dbr:ANSI/ISO_C_Specification_Language dbr:Dafny dbr:Greg_Nelson_(computer_scientist) dbr:Java_Modeling_Language dbr:Extended_static_checking dbr:List_of_tools_for_static_code_analysis dbr:ESC/Java2 dbr:Esc_java |
| is foaf:primaryTopic of | wikipedia-en:ESC/Java |