diff --git a/assignments/PA4/bad_inherit.cl b/assignments/PA4/bad_inherit.cl
index ba6b40f..c405155 100644
--- a/assignments/PA4/bad_inherit.cl
+++ b/assignments/PA4/bad_inherit.cl
@@ -34,15 +34,59 @@ class Err3 inherits String {};
 class Err3 inherits Bool {};
 class Err4 inherits Err3 {};*)
 class Err4 inherits Ok1 {
-    bye: SS <- 10;
+    bye: Bool <- 10;
     hello(a: TT) : NOEXIST { new Object };
 };
 
+(* the following case tests redefined attributes and methods *)
+(*
+class Err6Base {
+    dup_obj: Int <- 10; 
+    dup_method1(haha: Int): Int { 10 }; 
+    dup_method2(): Int { 10 }; 
+    dup_method3(): Int { 10 }; 
+    dup_method4(a:NOEXIST, b: Bool, c: NOEXIST): Int { a };
+};
+class Err6Sub inherits Err6Base {
+    dup_obj: Bool <- 20;
+    dup_obj: Bool <- 20;
+    dup_method1(fufu: Int): Int { 20 };
+    dup_method2(a:Int): Bool { false };
+    dup_method3(a:Int): Int { a };
+    dup_method4(a:NOEXIST, b: String, c: Bool): Int { a };
+};
+*)
 
-class Main inherits IO {
+
+class DummyMain {
+    la: Bool <- 20;
+    ala: Bool;
+    main(): Object {
+        { new DummyMain; }
+    };
+};
+
+class Main inherits DummyMain {
+    attr1: Bool <- (new Err5).hello();
+    attr2: Int <- (new Err5).bye();
     main(): Object {
         {
-            (new Err4).hell();
+            let x:Int in {
+                x1 <- x + 1;
+            };
+            (new Err4).hello(true);
+            (new Err4).hello();
         }
     };
+
+    main: Bool <- true;
+};
+
+class Err5 {
+    ala: Bool <- 20;
+    -- hello() : Object {{ala <- ala + 1;}};
+    hello: Int <- 20;
+    hello(): NOEXIST { new Object };
+    bye(): Bool { 10 };
+    -- ala: Int <- 20;
 };
\ No newline at end of file
diff --git a/assignments/PA4/cool-tree.h b/assignments/PA4/cool-tree.h
index 79f93bf..66b485d 100644
--- a/assignments/PA4/cool-tree.h
+++ b/assignments/PA4/cool-tree.h
@@ -247,6 +247,9 @@ public:
    Formal copy_Formal();
    void dump(ostream& stream, int n);
 
+   Symbol get_name() const { return name; };
+   Symbol get_type_decl() const { return type_decl; };
+
 #ifdef Formal_SHARED_EXTRAS
    Formal_SHARED_EXTRAS
 #endif
diff --git a/assignments/PA4/semant.cc b/assignments/PA4/semant.cc
index c4a9fbd..b30a252 100644
--- a/assignments/PA4/semant.cc
+++ b/assignments/PA4/semant.cc
@@ -1,11 +1,13 @@
 
 
 #include <cassert>
+#include <iostream>
 #include <stdlib.h>
 #include <stdio.h>
 #include <stdarg.h>
 #include <utility>
 #include <vector>
+#include <queue>
 #include "cool-tree.h"
 #include "semant.h"
 #include "utilities.h"
@@ -94,7 +96,6 @@ static void initialize_constants(void)
 ClassTable::ClassTable(Classes classes) : semant_errors(0) , error_stream(cerr) {
     install_basic_classes();
     /* first scan: de-duplicate class definitions*/
-    std::vector<class__class* > class_vec;
     for (auto i = classes->first(); classes->more(i); i = classes->next(i)) {
         auto class_i = static_cast<class__class*>(classes->nth(i));
         if (name_to_node.find(class_i->get_name()) != name_to_node.end()) {
@@ -104,7 +105,7 @@ ClassTable::ClassTable(Classes classes) : semant_errors(0) , error_stream(cerr)
             // null means we have this class, but not yet build inheritence graph for it
             name_to_node[class_i->get_name()] = new ClassGraphNode(class_i, nullptr);
             // discard redefined classes by constructing a new vector of classes
-            class_vec.push_back(class_i);
+            _class_vec.push_back(class_i);
         }
     }
 
@@ -113,7 +114,7 @@ ClassTable::ClassTable(Classes classes) : semant_errors(0) , error_stream(cerr)
     auto sym_Int = idtable.lookup_string("Int");
     auto sym_String = idtable.lookup_string("String");
     
-    for (auto class_i : class_vec) {
+    for (auto class_i : _class_vec) {
         auto sym_parent = class_i->get_parent();
         // Cool has restrictions on inheriting from the basic classes
         if ( sym_parent == sym_Bool || sym_parent == sym_Int || sym_parent == sym_String) {
@@ -139,9 +140,9 @@ ClassTable::ClassTable(Classes classes) : semant_errors(0) , error_stream(cerr)
     // Thus, we can start from object and mark all reachable nodes, error report those unreachable nodes
 
     /* third scan: check cyclic inheritance */
-    class_root->traverse();
+    class_root->traverse_reachable();
     for (auto i : name_to_node) {
-        if (!i.second->reachable()) {
+        if (!i.second->reachable) {
             semant_error(i.second->get_class()) << "Class `" << i.first 
                 << "` or its ancestor, is involved in an inheritance cycle.\n";
         }
@@ -149,40 +150,175 @@ ClassTable::ClassTable(Classes classes) : semant_errors(0) , error_stream(cerr)
     if (semant_errors) return;
     if (semant_debug) {
         std::cerr<< "Class Inheritance Analysis done.\n";
-        class_root->traverse(std::cout, 0);
+        class_root->traverse_dump_name(std::cout, 0);
     }
+}
+
+void ClassTable::symtab_dump(Symbol class_name) {
+    std::cerr << "SymTab of " << class_name << "\n";
+    std::cerr << "M(" << class_name << ") =";
+    symtab_met[class_name]->dump();
+    std::cerr << "O(" << class_name << ") =";
+    symtab_obj[class_name]->dump();
+    std::cerr << "--------\n\n";
+}
+
+Symbol ClassTable::symtab_object_lookup_parent(Symbol class_name, Symbol object_name) {
+    assert(name_to_node.find(class_name) != name_to_node.end());
+    auto class_node = name_to_node[class_name];
+    auto parent_node= class_node->parent;
+    while (parent_node) {
+        auto result = symtab_obj[parent_node->get_class()->get_name()]->probe(object_name);
+        // only need to lookup in the top scope, because attributes all reside in top scope
+        if (result) return result;
+        parent_node = parent_node->parent;
+    }
+    return nullptr;
+}
+
+method_class* ClassTable::symtab_method_lookup_parent(Symbol class_name, Symbol method_name) {
+    assert(name_to_node.find(class_name) != name_to_node.end());
+    auto class_node = name_to_node[class_name];
+    auto parent_node= class_node->parent;
+    while (parent_node) {
+        auto result = symtab_met[parent_node->get_class()->get_name()]->probe(method_name);
+        // only need to lookup in the top scope, because attributes all reside in top scope
+        if (result) return result;
+        parent_node = parent_node->parent;
+    }
+    return nullptr;
+}
+
+void ClassTable::install_all_features() {
     /* fourth scan: gather attr and method definition */
-    for (auto class_i : class_vec) {
-        auto features_i = class_i->get_features();
-        auto name_i = class_i->get_name();
-        symtab_met[name_i] = new SymbolTable<Symbol, method_class>;
-        symtab_obj[name_i] = new SymbolTable<Symbol, Entry>;
-        symtab_met[name_i]->enterscope();
-        symtab_obj[name_i]->enterscope();
-        for (auto j = features_i->first(); features_i->more(j); j = features_i->next(j)) {
-            auto feature_j = features_i->nth(j);
-            if (typeid(*feature_j) == typeid(attr_class)) {
-                auto attr_j = static_cast<attr_class*>(feature_j);
-                symtab_obj[name_i]->addid(attr_j->get_name(), attr_j->get_type_decl());
+    auto sym_Main = idtable.lookup_string("Main");
+    auto sym_main = idtable.lookup_string("main");
+    class__class* class_Main = nullptr;
+    method_class* method_main = nullptr; // main in class Main
+    std::queue<ClassGraphNode*> _iter_queue;
+    _iter_queue.push(class_root);
+    while (!_iter_queue.empty()) {
+        auto cur_node = _iter_queue.front();
+        _iter_queue.pop();
+        // std::cerr << "Pop " << cur_node->get_class()->get_name() << "\n";
+
+        for (auto child : cur_node->children) {
+            _iter_queue.push(child);
+            // std::cerr << "Push " << child->get_class()->get_name() << "\n";
+        }
+        auto cur_class = cur_node->get_class();
+        auto cur_name = cur_class->get_name();
+        if (cur_name == sym_Main) {
+            class_Main = cur_class;
+        }
+        symtab_met[cur_name] = new SymbolTable<Symbol, method_class>;
+        symtab_obj[cur_name] = new SymbolTable<Symbol, Entry>;
+        symtab_met[cur_name]->enterscope();
+        symtab_obj[cur_name]->enterscope();
+
+        auto cur_features = cur_class->get_features();
+        for (auto j = cur_features->first(); cur_features->more(j); j = cur_features->next(j)) {
+            auto cur_feature = cur_features->nth(j);
+            // std::cerr << "feature " << j << " ";
+            if (typeid(*cur_feature) == typeid(attr_class)) {
+                auto cur_attr = static_cast<attr_class*>(cur_feature);
+                // std::cerr << "attr " << cur_attr->get_name() << "\n";
+                if (symtab_obj[cur_name]->lookup(cur_attr->get_name()) != nullptr) {
+                    semant_error(cur_class->get_filename(), cur_attr) << "Attribute " << cur_attr->get_name() 
+                                            << " is multiply defined.\n";
+                }
+                else if (symtab_object_lookup_parent(cur_name, cur_attr->get_name()) != nullptr) {
+                    // check duplicate name for attributes
+                    semant_error(cur_class->get_filename(), cur_attr) << "Attribute " << cur_attr->get_name() 
+                                            << " is an attribute of an inherited class.\n";
+                }
+                else {
+                    symtab_obj[cur_name]->addid(cur_attr->get_name(), cur_attr->get_type_decl());
+                }
             }
-            else if (typeid(*feature_j) == typeid(method_class)) {
-                auto method_j = static_cast<method_class*>(feature_j);
-                symtab_met[name_i]->addid(method_j->get_name(), method_j);
+            else if (typeid(*cur_feature) == typeid(method_class)) {
+                auto cur_method = static_cast<method_class*>(cur_feature);
+                // std::cerr << "method " << cur_method->get_name() << "\n";
+                if (symtab_met[cur_name]->lookup(cur_method->get_name()) != nullptr) {
+                    semant_error(cur_class->get_filename(), cur_method) << "Method " << cur_method->get_name() 
+                                            << " is multiply defined.\n";
+                } 
+                else {
+                    auto overridden_method = symtab_method_lookup_parent(cur_name, cur_method->get_name());
+                    auto _error_flag = false;
+                    if (overridden_method != nullptr) {
+                        // additional check is necessary for overridden methods
+                        if (semant_debug) std::cerr << "Overriden method" << cur_method->get_name() << "\n";
+                        if (cur_method->get_return_type() != overridden_method->get_return_type()) {
+                            //  direct comaprison between Symbols is okay, 'cause Symbols(ptr to Entry) are distinct
+                            //      when talking about classes or types
+                            semant_error(cur_class->get_filename(), cur_method) 
+                                << "In redefined method " << cur_method->get_name() 
+                                << ", return type " << cur_method->get_return_type()
+                                << " is different from original return type" << overridden_method->get_return_type()
+                                << "\n";
+                            _error_flag = true;
+                        }
+                        else if (cur_method->get_formals()->len() != overridden_method->get_formals()->len()) {
+                            semant_error(cur_class->get_filename(), cur_method)
+                                << "Incompatible number of formal parameters in redefined method "
+                                << cur_method->get_name()
+                                << ".\n";
+                            _error_flag = true;
+                        }
+                        else {
+                            // we cannot directly compare 2 formal lists
+                            auto cur_formals = cur_method->get_formals();
+                            auto overridden_formals = overridden_method->get_formals();
+                            auto cur_formal_i = cur_formals->first();
+                            auto overridden_formal_i = overridden_formals->first();
+                            // by last check, we get ensured that their formal list should have the same length
+                            while (cur_formals->more(cur_formal_i)) {
+                                auto cur_formal = static_cast<formal_class*>(cur_formals->nth(cur_formal_i));
+                                auto overridden_formal = static_cast<formal_class*>(overridden_formals->nth(cur_formal_i));
+                                if (cur_formal->get_type_decl() != overridden_formal->get_type_decl()) {
+                                    semant_error(cur_class->get_filename(), cur_method) 
+                                        << "In redefined method " << cur_method->get_name() 
+                                        << ", parameter type " << cur_formal->get_type_decl()
+                                        << " is different from original type" << overridden_formal->get_type_decl()
+                                        << "\n";
+                                    _error_flag = true;
+                                    break;
+                                }
+                                cur_formal_i = cur_formals->next(cur_formal_i);
+                                overridden_formal_i = overridden_formals->next(overridden_formal_i);
+                            }
+                        }
+                    }
+                    if (!_error_flag) {
+                        // std::cerr << "method done " << cur_method->get_name() << "\n";
+                        symtab_met[cur_name]->addid(cur_method->get_name(), cur_method);
+                        if (class_Main != nullptr && cur_name == sym_Main && cur_method->get_name() == sym_main) {
+                            // main in class Main
+                            method_main = cur_method;
+                        }
+                    }
+                }
             }
             else assert(0);
         }
-    }
-    if (semant_debug) {
-        std::cerr << "Attr & Methods Collection done.\n";
-        for (auto class_i : class_vec) {
-            auto name_i = class_i->get_name();
-            std::cerr << "M(" << name_i << ") =";
-            symtab_met[name_i]->dump();
-            std::cerr << "O(" << name_i << ") =";
-            symtab_obj[name_i]->dump();
-            std::cerr << "--------\n\n";
+        if (semant_debug) {
+            symtab_dump(cur_name);
         }
     }
+
+    if (!class_Main) {
+        semant_error() << "Class Main is not defined.\n";
+        return;
+    }
+    else if (!method_main) {
+        semant_error(class_Main) << "No 'main' method in class Main.\n";
+        return;
+    }
+    else
+    if (semant_debug) {
+        std::cerr << "Attrs & Methods Collection done.\n";
+    }
 }
 
 void ClassTable::install_basic_classes() {
@@ -299,7 +435,7 @@ void ClassTable::install_basic_classes() {
 
     if (semant_debug) {
         std::cout << "Basic classed installed\n";
-        class_root->traverse(std::cout, 0);
+        class_root->traverse_dump_name(std::cout, 0);
     }
 }
 
@@ -362,11 +498,12 @@ void program_class::semant()
 	cerr << "Compilation halted due to static semantic errors." << endl;
 	exit(1);
     }
-    for (auto i = classes->first(); classes->more(i); i = classes->next(i)) {
-        auto class_i = static_cast<class__class*>(classes->nth(i));
+    /* Gather declared types of features for later use */
+    classtable->install_all_features();
+    /* Top down type checking */
+    for (auto class_i : classtable->class_vec()) {
         class_i->semant();
     }
-    /* some semantic analysis code may go here */
 
     if (classtable->errors()) {
 	cerr << "Compilation halted due to static semantic errors." << endl;
diff --git a/assignments/PA4/semant.h b/assignments/PA4/semant.h
index c66946d..df33b36 100644
--- a/assignments/PA4/semant.h
+++ b/assignments/PA4/semant.h
@@ -2,6 +2,7 @@
 #define SEMANT_H_
 
 #include <assert.h>
+#include <cstddef>
 #include <iostream>
 #include <ostream>
 #include <vector>
@@ -24,14 +25,14 @@ typedef ClassTable *ClassTableP;
 // methods.
 
 class ClassGraphNode {
-private:
+public:
   // tree-shape relation maintainer
   ClassGraphNode* parent;
   std::vector<ClassGraphNode*> children;
   // the `class__class` object for which it builds graph
   Class_ self;
   // for cycle detection
-  int mark = 0;
+  int reachable = 0;
 
 public:
   // Note that, Class_ = Class__class*, itself is a ptr type, so just use it
@@ -82,30 +83,47 @@ public:
   /*
   * traverse and print class name
   */
-  void traverse(std::ostream& stream, int n) const {
+  void traverse_dump_name(std::ostream& stream, int n) const {
     dump_Symbol(stream, n, dynamic_cast<class__class*>(self)->get_name());
     for (auto child: children) {
-      child->traverse(stream, n + 2);
+      child->traverse_dump_name(stream, n + 2);
     }
   }
 
   /*
   * traverse and mark all reachable children
   */
-  void traverse() {
-    mark = 1;
+  void traverse_reachable() {
+    reachable = 1;
     for (auto child : children) {
-      child->traverse();
+      child->traverse_reachable();
     }
   }
 
-  bool reachable() {
-    return !(mark == 0);
+  class__class* get_class() {
+    return static_cast<class__class*>(self);
   }
 
-  Class_ get_class() {
-    return self;
-  }
+  // static void traverse_iter(ClassGraphNode* root) {
+  //   auto cur_node = root;
+  //   std::vector<size_t> stk;
+  //   stk.push_back(0);
+  //   std::cout << pad((stk.size()-1) * 4) << cur_node->get_class()->get_name() << "\n";
+  //   while (!stk.empty()) {
+  //     if (cur_node->children.size() == stk.back()) {
+  //       // we have finished all the children
+  //       stk.pop_back();
+  //       cur_node = cur_node->parent;
+  //       continue;
+  //     }
+  //     auto next_idx = stk.back();
+  //     stk.pop_back();
+  //     stk.push_back(next_idx + 1);
+  //     cur_node = cur_node->children[next_idx];
+  //     std::cout << pad((stk.size()) * 2) << cur_node->get_class()->get_name() << "\n";
+  //     stk.push_back(0);
+  //   }
+  // }
 };
 
 
@@ -115,6 +133,7 @@ class ClassTable {
 private:
   int semant_errors;
   void install_basic_classes();
+  void recursive_all_features();
   ostream& error_stream;
 
   // Root of the Inheritance Graph (hopefully it is a tree if the program is correct)
@@ -129,8 +148,16 @@ private:
   std::map<Symbol, SymbolTable<Symbol, Entry>* > symtab_obj;
   std::map<Symbol, SymbolTable<Symbol, method_class>*> symtab_met;
 
+  // Actually, it makes things easier to keep a list-shape copy of classes
+  std::vector<class__class*> _class_vec;
+
 public:
   ClassTable(Classes);
+  void install_all_features();
+  void symtab_dump(Symbol);
+  Symbol symtab_object_lookup_parent(Symbol, Symbol);
+  method_class* symtab_method_lookup_parent(Symbol, Symbol);
+  std::vector<class__class*>& class_vec() { return _class_vec; }
   int errors() { return semant_errors; }
   ostream& semant_error();
   ostream& semant_error(Class_ c);