mheiber · July 30, 2024 16:11
diff --git a/python.als b/python.als
 abstract sig Class {
   methods: set Method,
   parent: lone Class
 }

 sig AbstractClass, ConcreteClass extends Class {}

 sig MethodName {}

 abstract sig Method {
  method_name: one MethodName
 }

 sig ConcreteMethod extends Method {
  calls: set Call
 }

 sig AbstractMethod extends Method {}

 sig Call {
   receiver: Var,
   call_method_name: MethodName,
   resolves_to: Method
 }

 abstract sig Type {
   supertypes: set Type,
   names_class: Class
 }
 sig AbstractType, ConcreteType extends Type {}

 sig Var {
   var_ty: Type,
   var_points_to: one (Var + Class)
 }


 // --------------- Boring well-formedness conditions

 fact "no class is its own ancestor" {
   all c: Class | c not in c.^parent
 }

 fact "all methods are in classes, all calls are in methods, all `MethodName`s are used" {
  all m: Method | some c: Class | m in c.methods
  all call: Call | some m: Method | call in m.calls
  all mn: MethodName | some m: Method | m.method_name = mn
 }

 fact "concrete classes cannot have direct abstract methods" {
  all class: ConcreteClass | no m: AbstractMethod | m in class.methods
 }

 fact "a class must have all the method names of its parent" {
   all class: Class | all mn: class.parent.methods.method_name |
   mn in class.methods.method_name
 }

 fact "methods are only inherited from parents" {
  all disj class1, class2: Class |
  all m: class1.methods |
  m in class2.methods implies
      (class1 in class2.parent or class2 in class1.parent)
 }

 fact "concrete classes must have implementations for all methods" {
    all c: ConcreteClass | c.methods in ConcreteMethod
 }

 fact "A variable must have come (transitively) from naming a class" {
  all v: Var | one class: Class | class in v.^var_points_to
 }

 fact "method names are unique in a class" {
  all c: Class | all disj m1, m2: c.methods |
  disj[m1.method_name, m2.method_name]
 }

 // ---------------Runtime semantics

 fact "dynamic method resolution" {
  all call: Call | call.resolves_to = resolve[call]
 }
 

 // --------------- Pre-existing, obvious type-checking

 fact "typing: an abstract method cannot override a concrete method " {
    all class: Class | all disj m1, overridden: (class + class.parent).methods | 
    overridden in ConcreteMethod implies m1 in ConcreteMethod
 }

 fact "typing: method calls are well-typed. Example: in c.foo() (where c is a name for a class) foo must exist on that class" {
   all call: Call | one m: Method | static_resolve[call] = m
 }

 fact "typing: variable aliasing reflects subtyping" {
  // var lower: subtype = .....
  // var upper: supertype = lower
  all upper, lower: Var | lower in upper.var_points_to implies upper.var_ty in lower.var_ty.supertypes
 }


 // --------------- New typing rules
 fact "typing: aliasing rules" {
  all t1, t2: Type |
  // all rules share the same conclusion
  t2 in t1.supertypes implies (
 	rule_abstract_covariant[t1, t2] // TODO: reinstate
       // or rule_concrete_covariant[t1, t2]
      // or rule_concrete_to_abstract[t1, t2]
       // or rule_abstract_to_concrete[t1, t2]
  )
 }

 /*
 T inherits from U
 ----------------------------------
 AbstractType<T> <: AbstractType<U>
 */
 pred rule_abstract_covariant[t1, t2: Type] {
  t1 in AbstractType and t2 in AbstractType
  and inherits_from[t1, t2]
 }

 /*
 T inherits from U
 ----------------------------------
 ConcreteType<T> <: ConcreteType<U>
 */
 pred rule_concrete_covariant[t1, t2: Type] {
  t1 in ConcreteType and t2 in ConcreteType
  and inherits_from[t1, t2]
 }

 /*
 T inherits from U
 ----------------------------------
 ConcreteType<T> <: AbstractType<U>
 */
 pred rule_concrete_to_abstract[t1, t2: Type] {
  t1 in ConcreteType and t2 in AbstractType
  and inherits_from[t1, t2]
 }

 /*
 T inherits from U                       U is a concrete class
 ----------------------------------
 AbstractType<T> <: ConcreteType<U>
 */
 pred rule_abstract_to_concrete[t1: Type, t2: Type] {
  t1 in AbstractType and t2 in ConcreteType
  and inherits_from[t1, t2]
  // the last conjunct is important. Comment it out to see a counterexample showing unsafety
 //  and t2.names_class in ConcreteClass
 }


 fact "typing: can't call abstract methods through AbstractType" {
  all call: Call | 
    call.receiver.var_ty in AbstractType implies static_resolve[call] in ConcreteMethod
 }

 /*

 C         C is a concrete class
 -------------------------
 C: ConcreteType<C>

 */
 fact "C has type ConcreteType<C> when C is a concrete class" {
   all v: Var | all class: Class |
   (v.var_points_to = class and v.var_ty in ConcreteType) implies
   (class in ConcreteClass and v.var_ty.names_class = class)
 }

 /*
 A          A is an abstract class
 -------------------------
 A: AbstractType<A>
 */
 fact "C has type ConcreteType<C> when C is a concrete class" {
   all v: Var | all class: Class |
   (v.var_points_to = class and v.var_ty in AbstractType) implies
   (class in AbstractClass and v.var_ty.names_class = class)
 }

 // ------------- helpers

 fun resolve_var[v: Var]: one Class {
    {class: Class | class in v.^var_points_to} // guaranteed to be exactly one due to fact above
 }

 // c.foo() where c is a name for a class resolves to method foo of c *or a sub-class of c* at runtime
 fun resolve[call: Call]: Method {
    {m: Method | m.method_name = call.call_method_name and m in call.receiver.resolve_var.methods}
 }

 // c.foo() where c is a name for a class "statically resolves" to method foo of c
 fun static_resolve[call: Call]: Method {
    {m: Method | m.method_name = call.call_method_name and m in call.receiver.var_ty.names_class.methods}
 }

 pred inherits_from[descendent: Type, ancestor: Type] {
   ancestor.names_class in (descendent.names_class + descendent.names_class.^parent)
 }


 // ------------- pretty

 fact "non-essential eta rule for AbstractType that makes visualizations easier to read" {
   all t1, t2: AbstractType |
   t1.names_class = t2.names_class
   and t1.supertypes = t2.supertypes implies t2 = t1
 }


 fact "non-essential eta rule for ConcreteType that makes visualizations easier to read" {
   all t1, t2: ConcreteType |
   t1.names_class = t2.names_class
   and t1.supertypes = t2.supertypes implies t2 = t1
 }

 // ------------make it interesting
 pred has_inherited_method {
  some m: Method | some disj c1, c2: Class | m in c1.methods and m in c2.methods
 }

 pred has_interesting_method_call {
  some call: Call | not (resolve[call] = static_resolve[call])
 }

 pred has_override {
  some m:  Method | some disj c1, c2: Class |
    { 
        c2 in c1.^parent
        m in c1.methods
        m not in c2.methods 
        m.method_name in c2.methods.method_name
    }
 }

 pred show { 
  // at least 1 method is abstract
  some am: AbstractMethod | am in univ
 }

 pred show_complicated {
  has_inherited_method
  has_interesting_method_call
  has_override
 }

 // -------------commands
 // run  show
 // run show_complicated for 4

 assert safe {  no c: Call | resolve[c] in AbstractMethod }
 check safe for 4 // up to 4 instances for every signature
 // check safe for 10
	abstract sig Class {
	methods: set Method,
	parent: lone Class
	}

	sig AbstractClass, ConcreteClass extends Class {}

	sig MethodName {}

	abstract sig Method {
	method_name: one MethodName
	}

	sig ConcreteMethod extends Method {
	calls: set Call
	}

	sig AbstractMethod extends Method {}

	sig Call {
	receiver: Var,
	call_method_name: MethodName,
	resolves_to: Method
	}

	abstract sig Type {
	supertypes: set Type,
	names_class: Class
	}
	sig AbstractType, ConcreteType extends Type {}

	sig Var {
	var_ty: Type,
	var_points_to: one (Var + Class)
	}


	// --------------- Boring well-formedness conditions

	fact "no class is its own ancestor" {
	all c: Class \| c not in c.^parent
	}

	fact "all methods are in classes, all calls are in methods, all `MethodName`s are used" {
	all m: Method \| some c: Class \| m in c.methods
	all call: Call \| some m: Method \| call in m.calls
	all mn: MethodName \| some m: Method \| m.method_name = mn
	}

	fact "concrete classes cannot have direct abstract methods" {
	all class: ConcreteClass \| no m: AbstractMethod \| m in class.methods
	}

	fact "a class must have all the method names of its parent" {
	all class: Class \| all mn: class.parent.methods.method_name \|
	mn in class.methods.method_name
	}

	fact "methods are only inherited from parents" {
	all disj class1, class2: Class \|
	all m: class1.methods \|
	m in class2.methods implies
	(class1 in class2.parent or class2 in class1.parent)
	}

	fact "concrete classes must have implementations for all methods" {
	all c: ConcreteClass \| c.methods in ConcreteMethod
	}

	fact "A variable must have come (transitively) from naming a class" {
	all v: Var \| one class: Class \| class in v.^var_points_to
	}

	fact "method names are unique in a class" {
	all c: Class \| all disj m1, m2: c.methods \|
	disj[m1.method_name, m2.method_name]
	}

	// ---------------Runtime semantics

	fact "dynamic method resolution" {
	all call: Call \| call.resolves_to = resolve[call]
	}


	// --------------- Pre-existing, obvious type-checking

	fact "typing: an abstract method cannot override a concrete method " {
	all class: Class \| all disj m1, overridden: (class + class.parent).methods \|
	overridden in ConcreteMethod implies m1 in ConcreteMethod
	}

	fact "typing: method calls are well-typed. Example: in c.foo() (where c is a name for a class) foo must exist on that class" {
	all call: Call \| one m: Method \| static_resolve[call] = m
	}

	fact "typing: variable aliasing reflects subtyping" {
	// var lower: subtype = .....
	// var upper: supertype = lower
	all upper, lower: Var \| lower in upper.var_points_to implies upper.var_ty in lower.var_ty.supertypes
	}


	// --------------- New typing rules
	fact "typing: aliasing rules" {
	all t1, t2: Type \|
	// all rules share the same conclusion
	t2 in t1.supertypes implies (
	rule_abstract_covariant[t1, t2] // TODO: reinstate
	// or rule_concrete_covariant[t1, t2]
	// or rule_concrete_to_abstract[t1, t2]
	// or rule_abstract_to_concrete[t1, t2]
	)
	}

	/*
	T inherits from U
	----------------------------------
	AbstractType<T> <: AbstractType<U>
	*/
	pred rule_abstract_covariant[t1, t2: Type] {
	t1 in AbstractType and t2 in AbstractType
	and inherits_from[t1, t2]
	}

	/*
	T inherits from U
	----------------------------------
	ConcreteType<T> <: ConcreteType<U>
	*/
	pred rule_concrete_covariant[t1, t2: Type] {
	t1 in ConcreteType and t2 in ConcreteType
	and inherits_from[t1, t2]
	}

	/*
	T inherits from U
	----------------------------------
	ConcreteType<T> <: AbstractType<U>
	*/
	pred rule_concrete_to_abstract[t1, t2: Type] {
	t1 in ConcreteType and t2 in AbstractType
	and inherits_from[t1, t2]
	}

	/*
	T inherits from U U is a concrete class
	----------------------------------
	AbstractType<T> <: ConcreteType<U>
	*/
	pred rule_abstract_to_concrete[t1: Type, t2: Type] {
	t1 in AbstractType and t2 in ConcreteType
	and inherits_from[t1, t2]
	// the last conjunct is important. Comment it out to see a counterexample showing unsafety
	// and t2.names_class in ConcreteClass
	}


	fact "typing: can't call abstract methods through AbstractType" {
	all call: Call \|
	call.receiver.var_ty in AbstractType implies static_resolve[call] in ConcreteMethod
	}

	/*

	C C is a concrete class
	-------------------------
	C: ConcreteType<C>

	*/
	fact "C has type ConcreteType<C> when C is a concrete class" {
	all v: Var \| all class: Class \|
	(v.var_points_to = class and v.var_ty in ConcreteType) implies
	(class in ConcreteClass and v.var_ty.names_class = class)
	}

	/*
	A A is an abstract class
	-------------------------
	A: AbstractType<A>
	*/
	fact "C has type ConcreteType<C> when C is a concrete class" {
	all v: Var \| all class: Class \|
	(v.var_points_to = class and v.var_ty in AbstractType) implies
	(class in AbstractClass and v.var_ty.names_class = class)
	}

	// ------------- helpers

	fun resolve_var[v: Var]: one Class {
	{class: Class \| class in v.^var_points_to} // guaranteed to be exactly one due to fact above
	}

	// c.foo() where c is a name for a class resolves to method foo of c or a sub-class of c at runtime
	fun resolve[call: Call]: Method {
	{m: Method \| m.method_name = call.call_method_name and m in call.receiver.resolve_var.methods}
	}

	// c.foo() where c is a name for a class "statically resolves" to method foo of c
	fun static_resolve[call: Call]: Method {
	{m: Method \| m.method_name = call.call_method_name and m in call.receiver.var_ty.names_class.methods}
	}

	pred inherits_from[descendent: Type, ancestor: Type] {
	ancestor.names_class in (descendent.names_class + descendent.names_class.^parent)
	}


	// ------------- pretty

	fact "non-essential eta rule for AbstractType that makes visualizations easier to read" {
	all t1, t2: AbstractType \|
	t1.names_class = t2.names_class
	and t1.supertypes = t2.supertypes implies t2 = t1
	}


	fact "non-essential eta rule for ConcreteType that makes visualizations easier to read" {
	all t1, t2: ConcreteType \|
	t1.names_class = t2.names_class
	and t1.supertypes = t2.supertypes implies t2 = t1
	}

	// ------------make it interesting
	pred has_inherited_method {
	some m: Method \| some disj c1, c2: Class \| m in c1.methods and m in c2.methods
	}

	pred has_interesting_method_call {
	some call: Call \| not (resolve[call] = static_resolve[call])
	}

	pred has_override {
	some m: Method \| some disj c1, c2: Class \|
	{
	c2 in c1.^parent
	m in c1.methods
	m not in c2.methods
	m.method_name in c2.methods.method_name
	}
	}

	pred show {
	// at least 1 method is abstract
	some am: AbstractMethod \| am in univ
	}

	pred show_complicated {
	has_inherited_method
	has_interesting_method_call
	has_override
	}

	// -------------commands
	// run show
	// run show_complicated for 4

	assert safe { no c: Call \| resolve[c] in AbstractMethod }
	check safe for 4 // up to 4 instances for every signature
	// check safe for 10