Skip to content

Instantly share code, notes, and snippets.

@practicingruby

practicingruby/x.md

Created March 30, 2014 22:41
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save practicingruby/9881164 to your computer and use it in GitHub Desktop.
Save practicingruby/9881164 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
x.md

From http://www.cse.ohio-state.edu/~neelam/courses/788/lwb.pdf

A type specification contains the following information:

  • The type's name
  • A description of the type's value space
  • For each of the type's methods:
    • its name
    • its signature (including signalled exceptions)
    • its behavior in terms of preconditions and postconditions

Note that creators are missing. Creators are specified separately to make it easy for a type to have multiple implementations, to allow new creators to be added later, to allow subtypes to have different creators than their supertypes, and to make it more convenient to define subtypes. ... However, he absence of creators (in type definitions) means data type induction cannot be used to reason about invariant properties.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment