Commit e9883d12 by Jean-Christophe Filliâtre

### python: support for procedures (i.e. functions with no return)

parent 78ed1df4
 print("la multiplication dite russe") a = int(input("entrez a : ")) b = int(input("entrez b : ")) #@ assume b >= 0 p = a q = b if q < 0: p = -a q = -b #@ assert q >= 0 r = 0 while q > 0: #@ invariant 0 <= q and r + p * q == a * b ... ... @@ -15,5 +22,5 @@ while q > 0: p = p + p q = q // 2 print(r) print("a * b =", r) #@ assert r == a * b
 ... ... @@ -243,7 +243,11 @@ let def inc (id, idl, sp, bl) = let env = List.fold_left add_var env idl in let param id = id.id_loc, Some id, false, None in let params = List.map param idl in let fd = (params, None, block env bl, spec env sp) in let local bl id = let loc = id.id_loc in mk_expr ~loc (Elet (id, Gnone, mk_ref ~loc (mk_var ~loc id), bl)) in let bl = List.fold_left local (block env bl) idl in let fd = (params, None, bl, (* spec env *) sp) in let d = Dfun (id, Gnone, fd) in inc.new_pdecl id.id_loc d ... ...
 from random import randint # def swap(a, i, j): # # @ requires 0 <= i < len(a) and 0 <= j < len(a) # t = a[i] # a[i] = a[j] # a[j] = t def swap(a, i, j): #@ requires 0 <= i < len(a) and 0 <= j < len(a) t = a[i] a[i] = a[j] a[j] = t i = randint(0, 10) #@ assert 0 <= i <= 10 ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment