### new example for balance

parent 37162168
 ... ... @@ -50,3 +50,67 @@ module Balance if balls < balls then 6 else 7 end module Balance12 use import int.Int use import array.Array (* All values in balls[lo..hi[ are equal to [w], apart from balls[lb] which is of a different weight (lighter or heavier) . *) predicate spec (balls: array int) (lo hi j: int) (w: int) (b: bool) = 0 <= lo <= j < hi <= length balls && (forall i: int. lo <= i < hi -> i <> j -> balls[i] = w) && (if b then balls[j] < w else balls[j] > w) (* j : the index of the different ball, b : the status (lighter or heavier) of the different ball False True meaning heavier and True meaining lighter *) let solve12 (balls: array int) (ghost w j: int) (ghost b: bool) : (int, bool) requires { spec balls 0 12 j w b } ensures { result = (j, b) } = if balls + balls + balls + balls = balls + balls + balls + balls then if balls + balls = balls + balls then if balls < balls then (11, False) else (11, True) else if balls + balls < balls + balls then if balls = balls then (8, True) else if balls < balls then (10, False) else (9, False) else if balls = balls then (8, False) else if balls < balls then (9, True) else (10, True) else if balls + balls + balls + balls < balls + balls + balls + balls then if balls + balls + balls = balls + balls + balls then if balls = balls then (3, True) else if balls < balls then (7, False) else (6, False) else if balls + balls + balls < balls + balls + balls then if balls = balls then (5, False) else if balls < balls then (0, True) else (1, True) else if balls = balls then (2, True) else (4, False) else if balls + balls + balls = balls + balls + balls then if balls = balls then (3, False) else if balls < balls then (6, True) else (7, True) else if balls + balls + balls < balls + balls + balls then if balls = balls then (4, True ) else if balls < balls then (5, False) else (2, False) else if balls = balls then (5, True) else if balls < balls then (1, False) else (0, False) end \ No newline at end of file
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
{"ft_lang_label":"__label__en","ft_lang_prob":0.53549796,"math_prob":0.9981781,"size":2398,"snap":"2020-10-2020-16","text_gpt3_token_len":909,"char_repetition_ratio":0.3132832,"word_repetition_ratio":0.22347629,"special_character_ratio":0.44245204,"punctuation_ratio":0.109561756,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9999101,"pos_list":[0,1,2],"im_url_duplicate_count":[null,null,null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2020-04-01T15:02:45Z\",\"WARC-Record-ID\":\"<urn:uuid:94a73017-215f-46af-a6e0-e50f4749a105>\",\"Content-Length\":\"133128\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:3c336315-4702-4574-bc56-1926e2e7777a>\",\"WARC-Concurrent-To\":\"<urn:uuid:9c033eba-8335-4a8a-b56b-1e4b08a86ddc>\",\"WARC-IP-Address\":\"128.93.193.8\",\"WARC-Target-URI\":\"https://gitlab.inria.fr/why3/why3/-/commit/24fc5f1618969fee61a96c7641fafc3bba1336ee\",\"WARC-Payload-Digest\":\"sha1:R3SY52MW4DUPE7Q4FOG3S75OWC3FYJBU\",\"WARC-Block-Digest\":\"sha1:4QN34YOKPVCXJ5DCTLP5QOEYQH5SBMSL\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2020/CC-MAIN-2020-16/CC-MAIN-2020-16_segments_1585370505731.37_warc_CC-MAIN-20200401130837-20200401160837-00540.warc.gz\"}"}