follow up with the spec change from .set_ to .with_

Author: Catoverflow

src/v2/controllers/vreplicaset_controller/trusted/exec_types.rs

@@ -73,14 +73,14 @@ impl VReplicaSet {
 
     #[verifier(external_body)]
     pub fn set_metadata(&mut self, metadata: ObjectMeta)
-        ensures self@ == old(self)@.set_metadata(metadata@),
+        ensures self@ == old(self)@.with_metadata(metadata@),
     {
         self.inner.metadata = metadata.into_kube();
     }
 
     #[verifier(external_body)]
     pub fn set_spec(&mut self, spec: VReplicaSetSpec)
-        ensures self@ == old(self)@.set_spec(spec@),
+        ensures self@ == old(self)@.with_spec(spec@),
     {
         self.inner.spec = spec.into_kube();
     }
@@ -207,21 +207,21 @@ impl VReplicaSetSpec {
 
     #[verifier(external_body)]
     pub fn set_replicas(&mut self, replicas: i32)
-        ensures self@ == old(self)@.set_replicas(replicas as int),
+        ensures self@ == old(self)@.with_replicas(replicas as int),
     {
         self.inner.replicas = Some(replicas);
     }
 
     #[verifier(external_body)]
     pub fn set_selector(&mut self, selector: LabelSelector)
-       ensures self@ == old(self)@.set_selector(selector@),
+       ensures self@ == old(self)@.with_selector(selector@),
     {
         self.inner.selector = selector.into_kube();
     }
 
     #[verifier(external_body)]
     pub fn set_template(&mut self, template: PodTemplateSpec)
-        ensures self@ == old(self)@.set_template(template@),
+        ensures self@ == old(self)@.with_template(template@),
     {
         self.inner.template = Some(template.into_kube());
     }

src/v2/controllers/vreplicaset_controller/trusted/spec_types.rs

@@ -30,14 +30,14 @@ impl VReplicaSetView {
         }
     }
 
-    pub open spec fn set_metadata(self, metadata: ObjectMetaView) -> VReplicaSetView {
+    pub open spec fn with_metadata(self, metadata: ObjectMetaView) -> VReplicaSetView {
         VReplicaSetView {
             metadata: metadata,
             ..self
         }
     }
 
-    pub open spec fn set_spec(self, spec: VReplicaSetSpecView) -> VReplicaSetView {
+    pub open spec fn with_spec(self, spec: VReplicaSetSpecView) -> VReplicaSetView {
         VReplicaSetView {
             spec: spec,
             ..self
@@ -175,21 +175,21 @@ impl VReplicaSetSpecView {
         }
     }
 
-    pub open spec fn set_replicas(self, replicas: int) -> VReplicaSetSpecView {
+    pub open spec fn with_replicas(self, replicas: int) -> VReplicaSetSpecView {
         VReplicaSetSpecView {
             replicas: Some(replicas),
             ..self
         }
     }
 
-    pub open spec fn set_selector(self, selector: LabelSelectorView) -> VReplicaSetSpecView {
+    pub open spec fn with_selector(self, selector: LabelSelectorView) -> VReplicaSetSpecView {
         VReplicaSetSpecView {
             selector: selector,
             ..self
         }
     }
 
-    pub open spec fn set_template(self, template: PodTemplateSpecView) -> VReplicaSetSpecView {
+    pub open spec fn with_template(self, template: PodTemplateSpecView) -> VReplicaSetSpecView {
         VReplicaSetSpecView {
             template: Some(template),
             ..self