seq X == {f:N -||-> X | dom f = 1..#f}
A sequence over X is a finite partial function (f) from the integers into X
such that the domain of f is the interval between 1 and the size of the
function. An example to illustrate the restriction on the domain:
A Sequence Not A Sequence 1 -> x 5 -> x 2 -> y 3 -> y 3 -> a 8 -> a 4 -> d 2 -> d
<s>i == s[i]Q. What is <s>0?
S1 S2 S1^S2 1 -> a 1 -> x 1 -> a 2 -> b 2 -> y 2 -> b 3 -> c 3 -> c (1+3 = 4) -> x (2+3 = 5) -> y
|^ : seq X x P X -> seq XSo, s |^ A means: take the sequence s, toss out any elements not in A, and squash the remaining parts of s back into a sequence (i.e. no gaps).
head: seq1 X -> XThat is, a total function. This is because we restrict the source of the function to non-empty sequences (seq1). We could also have given the signature for head as:
head: seq X -|-> XThat is, a partial function. Head is not defined for empty sequences, but we chose not to restrict the source of the function to non-empty sequences. Since there is an element in the source for which the function is undefined, it is partial.
If you define a function as partial, it's a nice idea to say what's excluded. In this case, dom head = seq X - {<>}.
The following two declarations are equivalent:
1) x : N; y : Z 2) --Name-------------------- | x : N | y : Z -------------------------- | ... --------------------------
The following two predicates are equivalent:
1) p1 ^ p2 (a conjunct) 2) --Name-------------------- | ... -------------------------- | p1 | p2 --------------------------
The operator "and" is implicit between the lines of a schema. The "or" operator must be written explicitly:
--Name-------------------- | ... -------------------------- | p1 v | p2 --------------------------
The "equal sign with the hat over it" means that it is a schema definition, i.e. a thing that can be type-checked.
--Editor----------------------------------------------- | text : seq CH | insertion : N -------------------------- | text != <> => insertion element_of dom text -------------------------------------------------------(Note that the lecture notes contain a typo in the last line of this schema: {} should be <>. This typo occurs throughout the lecture notes.) The last line is a condition which must always be satisfied (an invariant). It says that if the text is not empty, the insertion point must be somewhere within the text. It does not tell us anything about the insertion point if the text is empty.
An example of inclusion:
--R------- --S------- --S-------- | decl R | R | decl R ---------- | decl S | decl S | pred R ---------- ==> ----------- ---------- | pred S | pred S ---------- | pred R -----------Note that the precicates of S may refer to the declarations of R.
What about the case where R and S have variables with the same name?
--R------- --S------- | a : N | R | b : Z | a : N ---------- ---------- | pred R | pred S ---------- ----------R can be included in S because the variable name they have in common ("a") has the same type. If the type does not match, inclusion is not allowed.
Q. How strict is type compatibility? In other words, are a : N and a : R type compatible since N is a subset of R?
A. Types must match exactly. A type that is a subset of another is not
compatible with it.
The ability to rename schemas is convenient for an important aspect of usability: consistancy. Consistant behavior between the two applications is guaranteed (to some extent) because they are using the same abstract specification.
--Move Left---------------------------------- | A Editor --------------------- | insertion != 1 <- a precondition, the insertion point can't | already be a the left end | | text' = text <- must say what happens to each variable, | even if nothing happens | | insertion' = insertion - 1 ----------------------------------------------Precondidions can be easily identified because they don't involve any decorated variables.
If the schema does not say what happens to a variable, all we know about it is that the invarients in the original schema still hold--we may not know a specific value for the variable.
pos? element_of dom textinstead of
pos? < #textA. We use the domain restriction because it excludes numbers less than or equal to 0. Comparing to the length in the example above allows 0 as a valid position, which it is not.