 |
*********************************************************************
*** Chapter 1 - Foundation
*** Section 4: Constructors and Operator Attributes
***
*** SETS-AND-LISTS: sets down the fundamentals for the Set and List
*** sorts, including the main binary operator attributes "assoc,"
*** "comm," and "id: "
***
*********************************************************************
fmod SETS-AND-LISTS is
sorts Set List Elt .
subsort Elt < Set .
subsort Elt < List .
op nil : -> List [ctor] .
op none : -> Set [ctor] .
op _;_ : List List -> List [ctor assoc id: nil] .
op __ : Set Set -> Set [ctor assoc comm id: none] .
endfm
***********************************************************************
*** Chapter 1 - Foundation
*** Section 4: Constructors and Operator Attributes
***
*** PEANO-NAT : sets down the algebra for the Peano notation of the
*** natural numbers, using two constructors - the successor s and 0.
***
***********************************************************************
fmod PEANO-NAT is
sort Nat .
op 0 : -> Nat [ctor] .
op s : Nat -> Nat [ctor] .
endfm
********************************************************************
*** Chapter 1 - Foundation
*** Section 5: Kinds
***
*** ANIMALS : illustrates the use of kinds within connected
*** components using a dog-breeding model.
***
********************************************************************
fmod ANIMALS is
sorts Animal Vegetable Dog .
sorts Terrier Hound Toy Sporting .
subsort Dog < Animal .
subsorts Terrier Hound Toy Sporting < Dog .
ops bloodhound
collie
dalmatian
pitbull
schnauzer : -> Dog .
ops penguin
frog : -> Animal .
op bromeliad : -> Vegetable .
op breed : Dog Dog -> Dog [ctor] .
endfm
*** Chapter 1 - Foundation
*** Section 4: Constructors and Operator Attributes
***
*** SETS-AND-LISTS: sets down the fundamentals for the Set and List
*** sorts, including the main binary operator attributes "assoc,"
*** "comm," and "id: "
***
*********************************************************************
fmod SETS-AND-LISTS is
sorts Set List Elt .
subsort Elt < Set .
subsort Elt < List .
op nil : -> List [ctor] .
op none : -> Set [ctor] .
op _;_ : List List -> List [ctor assoc id: nil] .
op __ : Set Set -> Set [ctor assoc comm id: none] .
endfm
***********************************************************************
*** Chapter 1 - Foundation
*** Section 4: Constructors and Operator Attributes
***
*** PEANO-NAT : sets down the algebra for the Peano notation of the
*** natural numbers, using two constructors - the successor s and 0.
***
***********************************************************************
fmod PEANO-NAT is
sort Nat .
op 0 : -> Nat [ctor] .
op s : Nat -> Nat [ctor] .
endfm
********************************************************************
*** Chapter 1 - Foundation
*** Section 5: Kinds
***
*** ANIMALS : illustrates the use of kinds within connected
*** components using a dog-breeding model.
***
********************************************************************
fmod ANIMALS is
sorts Animal Vegetable Dog .
sorts Terrier Hound Toy Sporting .
subsort Dog < Animal .
subsorts Terrier Hound Toy Sporting < Dog .
ops bloodhound
collie
dalmatian
pitbull
schnauzer : -> Dog .
ops penguin
frog : -> Animal .
op bromeliad : -> Vegetable .
op breed : Dog Dog -> Dog [ctor] .
endfm