1/* 2 * Copyright (c) 2021-2022 Huawei Device Co., Ltd. 3 * Licensed under the Apache License, Version 2.0 (the "License"); 4 * you may not use this file except in compliance with the License. 5 * You may obtain a copy of the License at 6 * 7 * http://www.apache.org/licenses/LICENSE-2.0 8 * 9 * Unless required by applicable law or agreed to in writing, software 10 * distributed under the License is distributed on an "AS IS" BASIS, 11 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. 12 * See the License for the specific language governing permissions and 13 * limitations under the License. 14 */ 15 16module java_typing 17 18abstract sig Type { subtypes: set Type } 19one sig Top extends Type {} { no Top.~@subtypes } 20one sig Bot extends Type {} { no Bot.@subtypes } 21 22sig Class, Interface extends Type {} 23one sig Object extends Type {} 24one sig NullType extends Type {} 25 26let ProperType = Type - Top - Bot - NullType 27 28fact TypeHierarchy { 29 ProperType in Object.*subtypes 30 no t: ProperType | t in t.^subtypes 31 all c: Class | lone c.~subtypes & Class 32 all t: ProperType + NullType | t in Bot.~subtypes and t in Top.subtypes 33 all i: Interface | no i.~subtypes & Class 34 all i: ProperType | NullType in i.subtypes 35 NullType not in NullType.subtypes 36} 37 38abstract sig Value {type: Class + NullType} 39 40sig Instance extends Value {} { type in Class} 41one sig Null extends Value {} { type = NullType} 42 43sig Register {holds: one Value, type: Type} 44fact Soundness { all r: Register | r.holds.type in r.type.*subtypes } 45pred NonNull[r: Register] { r.type != NullType } 46pred Valid[r: Register] { r.type in ProperType } 47