StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p>In fact there is. There is a form of specification for functional languages based on Abstract Data Types called algebraic specification. Their behavior is very similar to that of objects in some ways, however the constructs are logical and mathematical, and are immutable like functional constructs.</p> <p>A particular functional specification language that's used in the Algorithms and Data Structures class in the University of Buenos Aires has generators, observers, and additional operations. A generator is an expression that is both an instance and a possible composition of the data type. For example, for a binary tree (ADT bt), we have null nodes, and binary nodes. So we would have the generators:</p> <pre><code>-nil -bin(left:bt, root: a, right:bt) </code></pre> <p>Where left is an instance of a bt, the root is a generic value, and right is another bt. So, nil is a valid form of a bt, but bin(bin(nil,1,nil),2,nil) is also valid, representing a binary tree with a root node with a value of 2, a left child node with a value of 1, and a null child right node.</p> <p>So for a function that say, calculates the number of nodes in a tree, you define an observer of the ADT, and you define a set of axioms which map to each generator. So, for example:</p> <pre><code>numberOfNodes(nil) == 0 numberOfNodes(bin(left,x,right))== 1 + numberOfNodes(left) + numberOfNodes(right) </code></pre> <p>This has the advantage of using recursive definitions of operations, and has the more, formally interesting property that you can use something called structural induction to PROVE that your specification is correct (yes, you demonstrate that your algorithm will produce the proper result).</p> <p>This is a fairly academic topic rarely seen outside of academic circles, but it's worth it to get an insight on program design that may change the way you think about algorithms and data structures. The proper bibliography includes:</p> <blockquote> <p>Bernot, G., Bidoit, M., and Knapik, T. 1995. Observational specifications and the indistinguishability assumption. Theor. Comput. Sci. 139, 1-2 (Mar. 1995), 275-314. DOI= <a href="http://dx.doi.org/10.1016/0304-3975(94)00017-D" rel="noreferrer">http://dx.doi.org/10.1016/0304-3975(94)00017-D</a></p> <p>Guttag, J. V. and Horning, J. J. 1993. Larch: Languages and Tools for Formal Specification. Springer-Verlag New York, Inc. Abstraction and Specification in Software Development, Barbara Liskov y John Guttag, MIT Press, 1986.</p> <p>Fundamentals of Algebraic Specification 1. Equations and Initial Semantics. H. Ehrig y B. Mahr Springer-Verlag, Berlin, Heidelberg, New York, Tokyo, Germany, 1985.</p> </blockquote> <p>With corresponding links: <a href="http://www.cs.st-andrews.ac.uk/~ifs/Resources/Notes/FormalSpec/AlgebraicSpec.pdf" rel="noreferrer">http://www.cs.st-andrews.ac.uk/~ifs/Resources/Notes/FormalSpec/AlgebraicSpec.pdf</a> <a href="http://nms.lcs.mit.edu/larch/pub/larchBook.ps" rel="noreferrer">http://nms.lcs.mit.edu/larch/pub/larchBook.ps</a></p> <p>It's a heck of an interesting topic.</p>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload