Abstract data types (model, principle without junk)

I have the following abstract data structure

Now I have to find a model that complies with the principle of "No Junk" and proves it

Could someone advise me to find a solution and understand the whole topic?

To thank

1 spec NatSet = Bool and Nat then
2
3 sorts
4 natSet = emptySet | add(natSet, nat)
5
6 ops
7 isEmpty: (natSet) bool,
8 contains: (natSet, nat) bool,
9 union: (natSet, natSet) natSet,
10 intersect: (natSet, natSet) natSet
11
12 vars
13 s,s’: natSet,
14 n,n’: nat
15
16 axioms
17 isEmpty(emptySet) = true
18 isEmpty(add(s, n)) = false
19
20 contains(emptySet, n) = false
21 contains(add(s, n), n) = true
22 n 6= n’ ⇒ contains(add(s, n), n’) = contains(s, n’)
23
24 union(emptySet, s) = s
25 union(add(s, n), s’) = add(union(s,s’), n)
26
27 intersect(emptySet, s’) = emptySet
28 intersect(s, emptySet) = emptySet
29 intersect(add(s, n), add(s’, n)) = add(intersect(s, s’), n)
30 n 6= n’ ⇒ intersect(add(s, n), add(s’, n’)) =
31 union(intersect(s, add(s’, n’)), intersect(add(s, n), s’))
32 end