Abstract: We design an extension of the join calculus with class-based inheritance. Method calls, locks, and states are handled in a uniform manner, using asynchronous messages. Classes are partial message definitions that can be combined and transformed by means of operators for behavioral and synchronization inheritance. We also give a polymorphic type system that statically enforces basic safety properties. Our language and its type system are compatible with the JoCaml implementation of the join calculus.

obj continuation = reply(n) |> out.print_int(n)

obj sbuffer = get(r) & put(n,s) |> r.reply(n) & s.reply()

obj abuffer = 
   put(n,r) |> r.reply() & abuffer.Some(n)
or get(r) & Some(n) |> r.reply(n)

obj buffer = 
   put(n,r) & Empty() |> r.reply() & buffer.Some(n)
or get(r)  & Some(n) |> r.reply(n) & buffer.Empty()
init buffer.Empty()

class buffer = self(z)
   get(r)  & Some(n) |> r.reply(n) & z.Empty()
or put(n,r) & Empty() |> r.reply() & z.Some(n)

obj b = buffer init b.Empty()

class logged_buffer = self(z)
   buffer
or log() & Some(n) |> out.print_int(n) & z.Some(n)
or log() & Empty() |> out.print_string("Empty") & z.Empty()

class logged_buffer_bis =
   match buffer with
     put(n,r) => put(n,r) |> out.print_int(n)
   end

class logged_buffer_bis = self(z)
   get(r)  & Some(n) |>  r.reply(n) & z.Empty()
or put(n,r) & Empty() |>  r.reply() & z.Some(n) & out.print_int(n)

class logged_buffer_ter = self(z)
   match buffer with
     put(n,r) => Parent_put(n,r) |> nil
   end
or put(n,r) |> out.print_int(n) & z.Parent_put(n,r)

1. All conjuncts M_i in the normal form of K are linear (as defined in Section 2.2) and binds the same names (i.e. have the same set of free names, as defined in Figure 4). By extension, we say that K binds the names fn(M_i) bound in each M_i, and write fn(K) for these names.
   
   
2. In a refinement clause K₁ Þ K₂ |> P, the pattern K₁ is either M or 0, the pattern K₂ binds at least the names of K₁ (fn(K₁)Í fn(K₂)), and K₁ is empty whenever K₂ is empty (so as to avoid the generation of empty patterns).

class buff = self (z)
   put(v,r) & (Empty(A, i, n) or Some(A, i, n)) |>
     r.reply() & z.Check(A[(i+n) mod A.size] <- v, i, n+1)
or get(r) & (Full(A, i, n) or Some(A, i, n)) |>
     r.reply(A[i]) & z.Check(A, (i+1) mod A.size, n-1)
or Check(A,i,n) |>
     if n = A.size then z.Full(A, i, n)
     else if n = 0 then z.Empty(A, i, n)
     else z.Some(A, i, n)
or Init(size) |> z.Empty(create(size), 0, 0)

Partitioning of acceptable states.

class buff2 = self(z)
   get2(r) & (Full(A,i,n) or Many(A, i, n)) |>
        r.reply(A[i], A[(i+1) mod A.size])
     &  z.Check(A, (i+2) mod A.size, n-2)
or match buff with
     Some(A, i, n) => (One(A, i, n) or Many(A, i, n)) |> nil
   end
or Some(A, i, n) |>
     if n > 1 then z.Many(A, i, n) else z.One(A, i, n)

History-dependent acceptable states.

class gget_buff = self (z)
   gget(r) & AfterPut() & (Full(A, i, n) or Some(A, i, n)) |>
        r.reply(A[i]) & z.NotAfterPut()
     &  z.Check(A, (i+1) mod A.size, n-1)
or match buff with
   Init(size) => Init(size) |> z.NotAfterPut()
 | put(v, r) =>
     put(v, r) & (AfterPut() or NotAfterPut()) |> z.AfterPut()
 | get(r) =>
     get(r) & (AfterPut() or NotAfterPut()) |> z.NotAfterPut()
end

Modification of acceptable states.

class locker = self (z)
   suspend(r) & Free() |> r.reply() & z.Locked()
or resume(r) & Locked() |> r.reply() & z.Free()

class locked_buff = self (z)
   locker
or match buff with
     Init(size) => Init(size) |> z.Free()
   | nil => Free() |> z.Free()
   end

Further anomalies

class buffer = self(z)
   get(r)  & Some(n) |> r.reply(n) & z.Empty()
or put(n,r) & Empty() |> r.reply() & z.Some(n)

obj server =
   do_incr(x,r) |> obj s = reply(n) |> x.put(n+1,r) in x.get(s)

class counter = self(z)
      match buffer with
        put(n,r) => put(n,r) & Exclusive() |> z.Exclusive() 
      end
   or match buffer with 
        put(n,r) => Put_priv(n,r) |> nil
      end
   or incr(r) & Exclusive() |> 
        obj s = reply() |> r.reply() & z.Exclusive() in 
        obj proxy = get(r) |> z.get(r) 
                 or put(n,r) |> z.Put_priv(n,r) in 
        server.do_incr(proxy,s) 
   or Init() |> z.Empty() & z.Exclusive()

class counter = self(z)
      match buffer with
        put(n,r) => Put_priv(n,r) |> nil
      end
   or put(n,r) & Exclusive() |> 
        obj s = reply(x) |> r.reply(x) & z.Exclusive() in
        z.Put_priv(n,s)
   or incr(r) & Exclusive() |> 
        obj s = reply() |> r.reply() & z.Exclusive() in 
        obj proxy = get(r) |> z.get(r) 
                 or put(n,r) |> z.Put_priv(n,r) in 
        server.do_incr(proxy,s) 
   or Init() |> z.Empty() & z.Exclusive()

• Class definitions are written class c(x) = I   C in P where
  • 
    
    the name c of the class takes a list of arguments (x);
    
    
  • I is a list of inheritance clauses of the form ( inherits c_i(u_i) as d_i) ^{i Î I} where each c_i is a previsouly defined class and d_i a local name for the body of c_i.
    
    
  • C is as before, except that it contains exactly one rule of the form c^init(x)|> Q. The names c^init are private and special in the sense that they cannot occur (in the user-language) anywhere else. Indeed, c^init play the role of class constructors.
    
    
  • P is as before.
  
  
  
• Object definitions are written obj x = c(u) in P where c has been defined as above.

• class c(x) = match C with c^init(x) Þ c^init(x) &^{i Î I} c_i^init (u_i) end in P
  
  
• obj x = c \ init c^init(u) in P.

obj join = sync1(r1) & sync2(r2) & Count(x) |>
   r1.reply() & r2.reply() & join.Count(x+1)

obj sbuffer = get(r) & put(n,s) |> r.reply(n) & s.reply()

1. If é K'ù = 0, we use cls(B^W,K Þ K') = W.
   (In this case, no new message with arguments is introduced.)
   
   
2. If dl(K) Ç W = Ø and é Kù ¹ 0, we use cls(B^W,K Þ K') = cl(K').
   (In this case, é Kù is a single message and é K''ù is empty.)
   
   
3. If dl(K) Ç W ¹ Ø, we use cls(B^W,K Þ K') = dl(é K'ù) È W.
   (In this case, all labels in é K''ù already appear in W.)
   
   
4. Otherwise (é Kù = 0 and é K'ù ¹ 0), we use cls(B^W,K Þ K') = dl(é K'ù) È dom(é Bù).

Processes.

Patterns.

Classes.

Refinement clauses.

class buffer = self(z)
     get(r)  & Some(a) |> r.reply(a) & z.Empty()
  or put(a,r) & Empty() |> r.reply() & z.Some(a)