diff --git a/src/two_k_11/challenge1.rs b/src/two_k_11/challenge1.rs
index feee794..451487d 100644
--- a/src/two_k_11/challenge1.rs
+++ b/src/two_k_11/challenge1.rs
@@ -2,12 +2,44 @@ use vstd::prelude::*;
 
 verus! {
 
+//datastructures
+// TO-DO: why do we specify these? For Tree-like problems?
+// [i32]
+//enddatastructures
+
+//preconditions
+// Encodes: A non-empty integer array a.
+pub fn precondition1(a: &[i32]) -> bool {
+    0 < a.len() <= usize::MAX
+}
+//endpreconditions
+
+//postconditions
+// TO-DO: Wonder how we'll make the signatures compatible.
+// Encodes: index re-turned by the method max() points to an element maximal in the array.
+pub fn postcondition1(a: &[i32], max_idx: usize) {
+    forall|i: int| 0 <= i < a.len() ==> a[max_idx as int] >= a[i]
+}
+//endpostconditions
+
+//specs
+spec pub fn preconditions(a: &[i32]) -> bool {
+    precondtion1(a)
+}
+
+spec pub fn postconditions(a: &[i32], max_idx: usize) {
+    postcondition1(a, max_idx)
+}
+//endspecs
+
 #[allow(unused)]
+//signature
 pub fn max(a: &[i32]) -> (max_idx: usize)
+//endsignature
     requires
-        0 < a.len() <= usize::MAX,
+        preconditions(a),
     ensures
-        forall|i: int| 0 <= i < a.len() ==> a[max_idx as int] >= a[i],
+        postconditions(a, max_idx),
 {
     let mut x = 0usize;
     let mut y = a.len() - 1;