- Referenced in 282 articles
- Using Z. Specification, refinement, and proof. The book is an in-depth introduction ... specification language $Z$. It is primarily directed to the user; the background theory is -- with ... integration of $Z$ with the refinement calculus and data refinement. The overall presentation is fluent ... adquate for promoting a discipline of formal specification and reasoning? Another disappointment is that...
- Referenced in 189 articles
- family of interface specification languages, with some elements of the refinement calculus...
- Referenced in 32 articles
- tree-based data structure allowing recursive grid refinements on a cell-by-cell basis ... dynamical tests to cosmological ones. The specific refinement strategy used in cosmological simulations is described...
- Referenced in 38 articles
- conformance of software components against state-machine specifications. To this aim, MAGIC extracts abstract software ... MAGIC verification engine, i.e., specification conformance using simulation and abstraction refinement. Viewing counterexamples as winning ... implementation and the specification, we describe an algorithm where abstractions are refined on the basis ... simultaneously. The refinement process is iterated until either a conformance with the specification is established...
- Referenced in 67 articles
- their specifications. ProB also contains a model checker and a refinement checker, both of which...
- Referenced in 313 articles
- linear shallow-water equations Adaptive mesh refinement: the resolution is adapted dynamically to the features ... Unlimited number of advected/diffused passive tracers Flexible specification of additional source terms Portable parallel support...
- Referenced in 21 articles
- csp2B means that abstract specifications and refinements may be specified purely using CSP or using...
- Referenced in 25 articles
- used to examine the specification, built models, construct refinements, and much more...
- Referenced in 15 articles
- that meets the requirements, and (b) refining that specification into code. More emphasis is commonly...
- Referenced in 57 articles
- Standard ML. ProofPower provides support for specification and proof in Z using a semantic embedding ... into HOL. The DAZ tool supporting refinement of Z to the SPARK subset...
- Referenced in 18 articles
- manipulate and transform JSL specifications by abstraction and refinement; the JaKarTa Prover Interface...
- Referenced in 232 articles
- variety of definitional, algorithmic and statistical refinements described here permits the execution time ... alignments produced by BLAST into a position-specific score matrix, and searching the database using...
- Referenced in 14 articles
- querying a relational database. These specifications are then iteratively refined into efficient implementations via automated ... that the synthesized program meets the original specification. Code synthesized by Fiat can be extracted...
- Referenced in 5 articles
- current FOP languages in expressing incremental refinements. Specifically, we outline five key problems and present...
- Referenced in 4 articles
- puts special emphasis on compositional refinement of both specifications and programs. It has an associated ... temporal logic, formal refinement notions, and program transformation rules. In this paper we extend this ... modeled and used during formal program specification and refinement. We exemplify our formalism...
- Referenced in 14 articles
- Refinement Calculus for Z. The fact that Z is a specification language only, with ... answer to that, we present ZRC, a refinement calculus based on Morgan’s work that ... conventions. This work builds upon existing refinement techniques for Z, but distinguishes itself mainly ... programs can be derived from Z specifications using ZRC. We present ZRC-L, the language...
- Referenced in 26 articles
- refinement calculus supporting the verification and derivation of programs against their specifications. A representative selection...
- Referenced in 3 articles
- Dtre) for the specification and verified refinement of specifications using operations on abstract data types ... centered around inductive sorts. Abstract specifications (theories) are refined in a stepwise fashion into increasingly ... more concrete theories. Our primary method of refinement is based on theory interpretation ... between types and their implementations; thus permitting specification to proceed independently of implementation while simultaneously...
- Referenced in 8 articles
- technique of stepwise refining a relational specification to a program by algebraic rules. The program...
- Referenced in 7 articles
- routine forchecking refinements among TMSC specifications; and (iii) a capability for generatingdiagnostic information ... tests when one system fails to refine another...