| library; |
| import self as self; |
| import "dart:core" as core; |
| import "dart:collection" as col; |
| |
| static method main() → dynamic { |
| final core::List<core::int> aList = block { |
| final core::List<core::int> #t1 = <core::int>[1]; |
| if(self::oracle() as{TypeError,ForDynamic} core::bool) |
| #t1.{core::List::add}{Invariant}(2){(core::int) → void}; |
| if(self::oracle() as{TypeError,ForDynamic} core::bool) |
| #t1.{core::List::add}{Invariant}(3){(core::int) → void}; |
| else |
| #t1.{core::List::add}{Invariant}(1.{core::int::unary-}(){() → core::int}){(core::int) → void}; |
| if(self::oracle() as{TypeError,ForDynamic} core::bool) |
| if(self::oracle() as{TypeError,ForDynamic} core::bool) |
| #t1.{core::List::add}{Invariant}(4){(core::int) → void}; |
| for (core::int i in <core::int>[5, 6, 7]) |
| #t1.{core::List::add}{Invariant}(i){(core::int) → void}; |
| for (core::int i in <core::int>[8, 9, 10]) |
| if(self::oracle() as{TypeError,ForDynamic} core::bool) |
| #t1.{core::List::add}{Invariant}(i){(core::int) → void}; |
| for (core::int i = 11; i.{core::num::<=}(14){(core::num) → core::bool}; i = i.{core::num::+}(1){(core::num) → core::int}) |
| #t1.{core::List::add}{Invariant}(i){(core::int) → void}; |
| } =>#t1; |
| final core::Set<core::int> aSet = block { |
| final core::Set<core::int> #t2 = col::LinkedHashSet::•<core::int>(); |
| #t2.{core::Set::add}{Invariant}(1){(core::int) → core::bool}; |
| if(self::oracle() as{TypeError,ForDynamic} core::bool) |
| #t2.{core::Set::add}{Invariant}(2){(core::int) → core::bool}; |
| if(self::oracle() as{TypeError,ForDynamic} core::bool) |
| #t2.{core::Set::add}{Invariant}(3){(core::int) → core::bool}; |
| else |
| #t2.{core::Set::add}{Invariant}(1.{core::int::unary-}(){() → core::int}){(core::int) → core::bool}; |
| if(self::oracle() as{TypeError,ForDynamic} core::bool) |
| if(self::oracle() as{TypeError,ForDynamic} core::bool) |
| #t2.{core::Set::add}{Invariant}(4){(core::int) → core::bool}; |
| for (core::int i in <core::int>[5, 6, 7]) |
| #t2.{core::Set::add}{Invariant}(i){(core::int) → core::bool}; |
| for (core::int i in <core::int>[8, 9, 10]) |
| if(self::oracle() as{TypeError,ForDynamic} core::bool) |
| #t2.{core::Set::add}{Invariant}(i){(core::int) → core::bool}; |
| for (core::int i = 11; i.{core::num::<=}(14){(core::num) → core::bool}; i = i.{core::num::+}(1){(core::num) → core::int}) |
| #t2.{core::Set::add}{Invariant}(i){(core::int) → core::bool}; |
| } =>#t2; |
| final core::Map<core::int, core::int> aMap = block { |
| final core::Map<core::int, core::int> #t3 = <core::int, core::int>{}; |
| #t3.{core::Map::[]=}{Invariant}(1, 1){(core::int, core::int) → void}; |
| if(self::oracle() as{TypeError,ForDynamic} core::bool) |
| #t3.{core::Map::[]=}{Invariant}(2, 2){(core::int, core::int) → void}; |
| if(self::oracle() as{TypeError,ForDynamic} core::bool) |
| #t3.{core::Map::[]=}{Invariant}(3, 3){(core::int, core::int) → void}; |
| else |
| #t3.{core::Map::[]=}{Invariant}(1.{core::int::unary-}(){() → core::int}, 1.{core::int::unary-}(){() → core::int}){(core::int, core::int) → void}; |
| if(self::oracle() as{TypeError,ForDynamic} core::bool) |
| if(self::oracle() as{TypeError,ForDynamic} core::bool) |
| #t3.{core::Map::[]=}{Invariant}(4, 4){(core::int, core::int) → void}; |
| for (core::int i in <core::int>[5, 6, 7]) |
| #t3.{core::Map::[]=}{Invariant}(i, i){(core::int, core::int) → void}; |
| for (core::int i in <core::int>[8, 9, 10]) |
| if(self::oracle() as{TypeError,ForDynamic} core::bool) |
| #t3.{core::Map::[]=}{Invariant}(i, i){(core::int, core::int) → void}; |
| for (core::int i = 11; i.{core::num::<=}(14){(core::num) → core::bool}; i = i.{core::num::+}(1){(core::num) → core::int}) |
| #t3.{core::Map::[]=}{Invariant}(i, i){(core::int, core::int) → void}; |
| } =>#t3; |
| core::print(aList); |
| core::print(aSet); |
| core::print(aMap); |
| } |
| static method oracle() → dynamic |
| return true; |