 | This article has not yet been rated on Wikipedia's content assessment scale. |
|
|
More Background Info Information
Quoting some contents from the manufacturer's webpage here to encourage inclusion of some of the details in the actual wikipedia entry, if this should turn out to be unacceptable, please feel free to remove the contents but leave the link, thanks!
Taken from http://www.praxis-his.com/sparkada/language.asp:
"SPARK is a subset of the Ada language. It includes Ada constructs regarded as essential for the construction of complex software, such as packages, private types, typed constants, functions with structured values, and the library system. It excludes tasks, exceptions, generic units, access types, use clauses, type aliasing, anonymous types, default values in record declarations, default subprogram parameters, goto statements, and declare statements."
Might make sense to incorporate some of this info by summarizing and rewording the essentials of it.
Also:
"Mandatory Annotations The requirements for analysis and verification imply a need for (non-Ada) formal comments which supply extra information to the SPARK tools. These annotations include: • global definitions in procedures (which declare 'imported' or 'exported' global variables) or functions (which import such variables); • dependency relations in procedures (which specify the imported variables which are required to derive the value of each exported variable); • the inherit clause in a SPARK package declaration (which restricts penetration of the package to items specifically imported from other packages); • the own variable clause in a SPARK package specification (which makes actions on the package state visible to analysis tools); • the initialisation annotation in a SPARK package specification (which indicates the initialisation by the package of its own state).
"
And:
"Proof Contexts These are special non-mandatory annotations which support the formal proof of SPARK programs. They are written in an expression language which is an extension of Ada's. Each proof context is associated with a particular location in the code: • the precondition of a procedure or function is associated with the begin of its body: it specifies conditions under which the procedure or function should be called; • the postcondition of a procedure (or the return annotation of a function) is associated with the end of the subprogram body: it defines the expected final state; • each assert statement (eg a loop invariant) or check statement (ie a well-formation statement) is located between two executable statements: it specifies the state expected of the program at that point. " —Preceding unsigned comment added by Parallelized ( talk • contribs) 11:44, 28 January 2008 (UTC)
| This article has not yet been rated on Wikipedia's content assessment scale. |
|
|
More Background Info Information
Quoting some contents from the manufacturer's webpage here to encourage inclusion of some of the details in the actual wikipedia entry, if this should turn out to be unacceptable, please feel free to remove the contents but leave the link, thanks!
Taken from http://www.praxis-his.com/sparkada/language.asp:
"SPARK is a subset of the Ada language. It includes Ada constructs regarded as essential for the construction of complex software, such as packages, private types, typed constants, functions with structured values, and the library system. It excludes tasks, exceptions, generic units, access types, use clauses, type aliasing, anonymous types, default values in record declarations, default subprogram parameters, goto statements, and declare statements."
Might make sense to incorporate some of this info by summarizing and rewording the essentials of it.
Also:
"Mandatory Annotations The requirements for analysis and verification imply a need for (non-Ada) formal comments which supply extra information to the SPARK tools. These annotations include: • global definitions in procedures (which declare 'imported' or 'exported' global variables) or functions (which import such variables); • dependency relations in procedures (which specify the imported variables which are required to derive the value of each exported variable); • the inherit clause in a SPARK package declaration (which restricts penetration of the package to items specifically imported from other packages); • the own variable clause in a SPARK package specification (which makes actions on the package state visible to analysis tools); • the initialisation annotation in a SPARK package specification (which indicates the initialisation by the package of its own state).
"
And:
"Proof Contexts These are special non-mandatory annotations which support the formal proof of SPARK programs. They are written in an expression language which is an extension of Ada's. Each proof context is associated with a particular location in the code: • the precondition of a procedure or function is associated with the begin of its body: it specifies conditions under which the procedure or function should be called; • the postcondition of a procedure (or the return annotation of a function) is associated with the end of the subprogram body: it defines the expected final state; • each assert statement (eg a loop invariant) or check statement (ie a well-formation statement) is located between two executable statements: it specifies the state expected of the program at that point. " —Preceding unsigned comment added by Parallelized ( talk • contribs) 11:44, 28 January 2008 (UTC)