Trait implementation method refinement Choosing alternative C as discussed in pp 19-23 In other words, any pre-/post-condition provided by `other` will overwrite any provided by `self`.
(&self, other: &Self)
| 368 | /// In other words, any pre-/post-condition provided by `other` will overwrite any provided by |
| 369 | /// `self`. |
| 370 | pub fn refine(&self, other: &Self) -> Self { |
| 371 | let pres = if other.pres.is_empty() { |
| 372 | self.pres.clone() |
| 373 | } else { |
| 374 | other.pres.clone() |
| 375 | }; |
| 376 | let posts = if other.posts.is_empty() { |
| 377 | self.posts.clone() |
| 378 | } else { |
| 379 | other.posts.clone() |
| 380 | }; |
| 381 | let pledges = if other.pledges.is_empty() { |
| 382 | self.pledges.clone() |
| 383 | } else { |
| 384 | other.pledges.clone() |
| 385 | }; |
| 386 | let predicate_body = if other.predicate_body.is_none() { |
| 387 | self.predicate_body.clone() |
| 388 | } else { |
| 389 | other.predicate_body.clone() |
| 390 | }; |
| 391 | Self { |
| 392 | pres, |
| 393 | posts, |
| 394 | pledges, |
| 395 | predicate_body, |
| 396 | pure: other.pure, |
| 397 | trusted: other.trusted, |
| 398 | } |
| 399 | } |
| 400 | } |
| 401 | |
| 402 | #[derive(Debug, Clone)] |