Software Engineering Documentation

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.

====== set[T] in Prelude ======

<code>
sets [T: TYPE]: THEORY
 BEGIN
  set: TYPE = [T -> bool]
  t, t1, t2: VAR T
  s, s1, s2, s3: VAR set
  p: VAR pred[T]

  member(x, s): bool = s(x)

  empty?(s): bool = (FORALL t: NOT member(t, s))

  emptyset: set = {t | false}

  nonempty?(s): bool = NOT empty?(s)

  % In PVS, (nonempty?) coerces boolean function nonempty? into a Type
  add(t1, s): (nonempty?) = {t2 | t2 = t1 OR member(t2, s)}

  remove(t1, s): set = {t2 | t2 /= t1 AND member(t2, s)}

  subset?(s1, s2): bool = (FORALL t: member(t, s1) => member(t, s2))

  union(s1, s2): set = {t | member(t, s1) OR member(t, s2)}

  intersection(s1, s2): set = {t | member(t, s1) AND member(t, s2)}

  disjoint?(s1, s2): bool = empty?(intersection(s1, s2))

  complement(s): set = {t | NOT member(t, s)} 

  difference(s1, s2): set = {t | member(t, s1) AND NOT member(t, s2)}

  singleton?(s): bool = (EXISTS (t1:(s)): (FORALL (t2:(s)): t1 = t2))

  singleton(t1): (singleton?) = {t2 | t2 = t1}

  ...
  % See Prelude for the full theory

 END sets
</code>

Software Engineering Documentation

User Tools

Site Tools

Page Tools