Add constructors

chapters/6-Encoding.typ

@@ -69,8 +69,10 @@ Encoding the receiver of a method is straightforward since the receiver is consi
 
 === Constructor
 
-- black-box Function
-- edge cases not supported at the moment
+Constructors are encoded as black-box methods returning a unique object. The encoding of a constructor requires access to the shared predicates for every property that is not of a primitive type. In addition, the unique predicate is also required for properties that are unique in the class declaration.
+Currently, the plugin only supports class properties declared as parameters. Properties declared within the body of a class and initializing blocks are not supported yet, as they may construct objects that are not necessarily unique.
+
+#code-compare("Constructor encoding", .8fr, constructor-kt, constructor-vpr, same-row: false)
 
 == Predicates Unfolding<cap:unfolding>
 

vars/kt-to-vpr-examples.typ

@@ -285,4 +285,29 @@ ensures acc(SharedT(t), wildcard)
   exhale acc(UniqueT(t), write)
   sharedParam(t)
 }
+```
+
+#let constructor-kt = ```kt
+class A(val x: Int, var y: Int)
+
+class B(@property:Unique var a1: A, var a2: A)
+```
+
+#let constructor-vpr = ```java
+method constructorA(p1: Int, p2: Int) returns (ret: Ref)
+  ensures acc(SharedA(ret), wildcard)
+  ensures acc(UniqueA(ret), write)
+  ensures unfolding acc(SharedA(ret), wildcard) in
+    ret.x == p1
+  ensures unfolding acc(UniqueA(ret), write) in
+    ret.x == p1 && ret.y == p2
+
+method constructorB(p1: Ref, p2: Ref) returns (ret: Ref)
+  requires acc(UniqueA(p1), write)
+  requires acc(SharedA(p1), wildcard)
+  requires acc(SharedA(p2), wildcard)
+  ensures acc(SharedB(ret), wildcard)
+  ensures acc(UniqueB(ret), write)
+  ensures unfolding acc(UniqueB(ret), write) in
+    ret.a1 == p1 && ret.a2 == p2
 ```