From 8f0d93a40c56fe1f4034b8d0a5cd1970687d6803 Mon Sep 17 00:00:00 2001 From: Orestis Melkonian <melkon.or@gmail.com> Date: Fri, 9 Feb 2018 21:11:35 +0100 Subject: [PATCH] README: model highlighting --- README.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 3ed6127..0ed8f4c 100644 --- a/README.md +++ b/README.md @@ -137,7 +137,7 @@ public static void test(int[] a) { ``` The resulting (raw) model: -```yaml +```scala a.null -> true a -> { 0 -> 1 @@ -147,7 +147,7 @@ a -> { ``` Essentially this model tells us that the two preconditions are not equivalent with an `a` that is both `null` and `[1, 0]`. A post-processing step has been added to pretty print the model and it shows: -```yaml +```scala a = null ``` @@ -168,7 +168,7 @@ public static void test2(int[] a) { ``` The resulting (raw) model: -```yaml +```scala a.length -> 1 a -> { 0 -> 0 @@ -178,7 +178,7 @@ a -> { ``` This model tells us that `a.length == 1` and that `a == [0, 1]` which is contradictory. A postprocessing step has been added to pretty print the model. And the result will instead show: -```yaml +```scala a = inconsistent array representation ``` -- GitLab